theory Overview_Demo imports Main begin (* A simple comment *) text {* This is also a comment but it generates nice \LaTeX-text! *} text {* Note that variables and constants (eg True, &) are displayed differently. *} term "True" term "False" term "true" term "true::bool" term "True & False" term "True & false" value "True & False" value "True & P" text{* To display types: menu Isabelle/Isar -> Settings -> Show Types *} text {* Warning: 0 and + are overloaded: *} term "n + n = 0" term "(n::nat) + n = 0" value "(\A. A & A) False" (* Try this: term "True + False" Terms must be type correct! *) text{* Type inference: *} term "f (g x) y" term "h (%x. f(g x))" term "%x. x + x" end