--- a/QuotMain.thy	Thu Sep 24 17:43:26 2009 +0200
+++ b/QuotMain.thy	Fri Sep 25 09:38:16 2009 +0200
@@ -77,8 +77,8 @@
 done
 
 lemma R_trans:
-  assumes ab: "R a b" 
-  and     bc: "R b c" 
+  assumes ab: "R a b"
+  and     bc: "R b c"
   shows "R a c"
 proof -
   have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
@@ -88,15 +88,15 @@
 qed
 
 lemma R_sym:
-  assumes ab: "R a b" 
+  assumes ab: "R a b"
   shows "R b a"
 proof -
   have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
   then show "R b a" using ab unfolding SYM_def by blast
 qed
 
-lemma R_trans2: 
-  assumes ac: "R a c" 
+lemma R_trans2:
+  assumes ac: "R a c"
   and     bd: "R b d"
   shows "R a b = R c d"
 proof
@@ -156,11 +156,11 @@
 ML {*
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
-let  
+let
   val typedef_tac =
      EVERY1 [rewrite_goal_tac @{thms mem_def},
-             rtac @{thm exI}, 
-             rtac @{thm exI}, 
+             rtac @{thm exI},
+             rtac @{thm exI},
              rtac @{thm refl}]
 in
   LocalTheory.theory_result
@@ -215,7 +215,7 @@
             rtac @{thm QUOT_TYPE.QUOTIENT},
             rtac quot_type_thm]
 in
-  Goal.prove lthy [] [] goal 
+  Goal.prove lthy [] [] goal
     (K typedef_quotient_thm_tac)
 end
 *}
@@ -925,7 +925,7 @@
 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
 ML {*
   Toplevel.program (fn () =>
-    Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
+    Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
   )
 *}
 
@@ -938,7 +938,7 @@
       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
       val [cmT, crT] = Thm.dest_ctyp cr2;
     in
-      Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
+      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
     end
 *}
 
@@ -949,7 +949,7 @@
       val (lop, larg) = Thm.dest_comb lhs;
       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
     in
-      Drule.instantiate' [SOME caT,SOME crT] [NONE,NONE,SOME lop] @{thm arg_cong}
+      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
     end
 *}
 
@@ -1001,7 +1001,7 @@
 *}
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1017,7 +1017,7 @@
 
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1029,7 +1029,7 @@
 
 thm m2
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1041,7 +1041,7 @@
 
 thm list_eq.intros(4)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
@@ -1075,7 +1075,7 @@
 ML {*
   Toplevel.program (fn () =>
     MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
-      Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz''
+      Drule.instantiate' [] [NONE, SOME (@{cpat "REP_fset x"})] zzz''
     )
   )
 *}
@@ -1083,11 +1083,11 @@
 
 thm list_eq.intros(5)
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
-  val cgoal = 
+  val cgoal =
     Toplevel.program (fn () =>
       cterm_of @{theory} goal
     )
@@ -1103,7 +1103,7 @@
 thm list.induct
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}
 ML {*
   val goal =
@@ -1126,7 +1126,7 @@
 thm card1_suc
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
 *}
 ML {*
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs