diff -r eed7ca453573 -r 3c9a0985e6be src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Mon Jan 11 07:44:20 2016 +0100
+++ b/src/CCL/CCL.thy	Mon Jan 11 21:16:38 2016 +0100
@@ -320,17 +320,17 @@
   apply blast
   done
 
-lemma POgenXH: 
-  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma POgenXH:
+  "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+           (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
            (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
   apply (unfold POgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma poXH: 
-  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |  
+lemma poXH:
+  "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
   apply (simp add: PO_iff del: ex_simps)
   apply (rule POgen_mono
@@ -438,18 +438,18 @@
   apply blast
   done
 
-lemma EQgenXH: 
-  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |  
-                                             (t=false \<and> t'=false) |  
-                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |  
+lemma EQgenXH:
+  "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |
+                                             (t=false \<and> t'=false) |
+                 (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
   apply (unfold EQgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
-lemma eqXH: 
-  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |  
-                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |  
+lemma eqXH:
+  "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
+                     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                      (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
   apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
     (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |