diff -r 2064f0fd20c9 -r f1db55c7534d src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Mon Apr 30 22:43:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed May 02 01:42:23 2007 +0200
@@ -1,6 +1,6 @@
 (* $Id$ *)
 
-(* A challenge suggested by Adam Chlipala *)
+(* The definitions for a challenge suggested by Adam Chlipala *)
 
 theory Compile
 imports "../Nominal"
@@ -8,51 +8,58 @@
 
 atom_decl name 
 
-nominal_datatype data = DNat
-                      | DProd "data" "data"
-                      | DSum "data" "data"
+nominal_datatype data = 
+    DNat
+  | DProd "data" "data"
+  | DSum "data" "data"
 
-nominal_datatype ty = Data "data"
-                    | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype ty = 
+    Data "data"
+  | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trm = Var "name"
-                     | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
-                     | App "trm" "trm"
-                     | Const "nat"
-                     | Pr "trm" "trm"
-                     | Fst "trm"
-                     | Snd "trm"
-                     | InL "trm"
-                     | InR "trm"
-                     | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" 
-                             ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
+nominal_datatype trm = 
+  Var "name"
+  | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
+  | App "trm" "trm"
+  | Const "nat"
+  | Pr "trm" "trm"
+  | Fst "trm"
+  | Snd "trm"
+  | InL "trm"
+  | InR "trm"
+  | Case "trm" "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" 
+          ("Case _ of inl _ \<rightarrow> _ | inr _ \<rightarrow> _" [100,100,100,100,100] 100)
 
 nominal_datatype dataI = OneI | NatI
 
-nominal_datatype tyI = DataI "dataI"
-                     | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
+nominal_datatype tyI = 
+    DataI "dataI"
+  | ArrowI "tyI" "tyI" ("_\<rightarrow>_" [100,100] 100)
 
-nominal_datatype trmI = IVar "name"
-                      | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
-                      | IApp "trmI" "trmI"
-                      | IUnit
-                      | INat "nat"
-                      | ISucc "trmI"
-                      | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
-                      | IRef "trmI" 
-                      | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
-                      | Iif "trmI" "trmI" "trmI"
+nominal_datatype trmI = 
+    IVar "name"
+  | ILam "\<guillemotleft>name\<guillemotright>trmI" ("ILam [_]._" [100,100] 100)
+  | IApp "trmI" "trmI"
+  | IUnit
+  | INat "nat"
+  | ISucc "trmI"
+  | IAss "trmI" "trmI" ("_\<mapsto>_" [100,100] 100)
+  | IRef "trmI" 
+  | ISeq "trmI" "trmI" ("_;;_" [100,100] 100)
+  | Iif "trmI" "trmI" "trmI"
 
 text {* valid contexts *}
 
-inductive2 valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
+inductive2 
+  valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
 | v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *)
 
 text {* typing judgements for trms *}
 
-inductive2 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
+inductive2 
+  typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
 | t1[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> \<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
@@ -69,7 +76,8 @@
 
 text {* typing judgements for Itrms *}
 
-inductive2 Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
+inductive2 
+  Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
 | t1[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : \<tau>1\<rightarrow>\<tau>2; \<Gamma> I\<turnstile> e2 : \<tau>1\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IApp e1 e2 : \<tau>2"
@@ -159,7 +167,8 @@
 
 text {* big-step evaluation for trms *}
 
-inductive2 big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
+inductive2 
+  big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
 where
   b0[intro]: "Lam [x].e \<Down> Lam [x].e"
 | b1[intro]: "\<lbrakk>e1\<Down>Lam [x].e; e2\<Down>e2'; e[x::=e2']\<Down>e'\<rbrakk> \<Longrightarrow> App e1 e2 \<Down> e'"
@@ -172,7 +181,8 @@
 | b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 | b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 
-inductive2 Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
+inductive2 
+  Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
 where
   m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
 | m1[intro]: "\<lbrakk>(m,e1)I\<Down>(m',ILam [x].e); (m',e2)I\<Down>(m'',e3); (m'',e[x::=e3])I\<Down>(m''',e4)\<rbrakk>