--- a/src/HOL/Nominal/Examples/Crary.thy Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Wed May 02 01:42:23 2007 +0200
@@ -14,15 +14,17 @@
atom_decl name
-nominal_datatype ty = TBase
- | TUnit
- | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty =
+ TBase
+ | TUnit
+ | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
-nominal_datatype trm = Unit
- | Var "name"
- | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
- | App "trm" "trm"
- | Const "nat"
+nominal_datatype trm =
+ Unit
+ | Var "name"
+ | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+ | App "trm" "trm"
+ | Const "nat"
types Ctxt = "(name\<times>ty) list"
types Subst = "(name\<times>trm) list"