--- a/src/HOL/Nominal/Examples/Height.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy Wed May 02 01:42:23 2007 +0200
@@ -8,9 +8,10 @@
atom_decl name
-nominal_datatype lam = Var "name"
- | App "lam" "lam"
- | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+nominal_datatype lam =
+ Var "name"
+ | App "lam" "lam"
+ | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
text {* definition of the height-function on lambda-terms *}