Isabelle/Isar Reference Manual
For a comprehensive guide on Isabelle commands
declare thms - declares theorems to the current local theory context. No theorem binding is involved here, unlike theorems or lemmas (cf.§5.11), so declare only has the efect of applying attributes as included in the theorem speci cation. Isar manual p85
Locales - A sectioning concept for Isabelle
Locales are a means to de fine local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants de fined locally and associated with pretty printing syntax. Locales can be seen as a simple form of modules. read more
Recursive Functions - Defining Recursive Functions in Isabelle/HOL
This tutorial describes the use of the new function package, which
provides general recursive function de nitions for Isabelle/HOL. We start
with very simple examples and then gradually move on to more advanced
topics such as manual termination proofs, nested recursion, partiality, tail
recursion and congruence rules. read tutorial
For a comprehensive guide on Isabelle commands
declare thms - declares theorems to the current local theory context. No theorem binding is involved here, unlike theorems or lemmas (cf.§5.11), so declare only has the efect of applying attributes as included in the theorem speci cation. Isar manual p85
Locales - A sectioning concept for Isabelle
Locales are a means to de fine local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants de fined locally and associated with pretty printing syntax. Locales can be seen as a simple form of modules. read more
Recursive Functions - Defining Recursive Functions in Isabelle/HOL
This tutorial describes the use of the new function package, which
provides general recursive function de nitions for Isabelle/HOL. We start
with very simple examples and then gradually move on to more advanced
topics such as manual termination proofs, nested recursion, partiality, tail
recursion and congruence rules. read tutorial
