# HG changeset patch
# User wenzelm
# Date 1415710256 -3600
# Node ID b38a54bbfbd6cd467849b7d18ff3d748e93032b5
# Parent  762ee71498fa86933c677eb377ff8dd3e7c2c35e
tuned whitespace;

diff -r 762ee71498fa -r b38a54bbfbd6 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CCL/CCL.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -230,7 +230,6 @@
   by simp
 
 ML {*
-
 local
   fun pairs_of f x [] = []
     | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)
@@ -259,11 +258,9 @@
   fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
   fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
 end
-
 *}
 
 ML {*
-
 val caseB_lemmas = mk_lemmas @{thms caseBs}
 
 val ccl_dstncts =
diff -r 762ee71498fa -r b38a54bbfbd6 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CCL/Term.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -91,7 +91,6 @@
          val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
      in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
       end;
-
 *}
 
 parse_translation {*
diff -r 762ee71498fa -r b38a54bbfbd6 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CCL/Type.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -100,9 +100,7 @@
   and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))"
   unfolding simp_type_defs by blast+
 
-ML {*
-ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs});
-*}
+ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *}
 
 
 subsection {* Canonical Type Rules *}
diff -r 762ee71498fa -r b38a54bbfbd6 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CCL/Wfd.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -411,7 +411,6 @@
 subsection {* Typechecking *}
 
 ML {*
-
 local
 
 val type_rls =
@@ -444,9 +443,11 @@
   in try_IHs rnames end)
 
 fun is_rigid_prog t =
-     case (Logic.strip_assums_concl t) of
-        (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a [])
-       | _ => false
+  (case (Logic.strip_assums_concl t) of
+    (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =>
+      null (Term.add_vars a [])
+  | _ => false)
+
 in
 
 fun rcall_tac ctxt i =
@@ -461,11 +462,10 @@
   match_tac ctxt [@{thm SubtypeI}] i
 
 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
-          if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
+    if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
 
 fun typechk_tac ctxt rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac ctxt rls)) i
 
-fun tac ctxt = typechk_tac ctxt [] 1
 
 (*** Clean up Correctness Condictions ***)
 
diff -r 762ee71498fa -r b38a54bbfbd6 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CTT/Arith.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -174,10 +174,10 @@
 local val congr_rls = @{thms congr_rls} in
 
 fun arith_rew_tac ctxt prems = make_rew_tac ctxt
-    (Arith_simp.norm_tac ctxt (congr_rls, prems))
+  (Arith_simp.norm_tac ctxt (congr_rls, prems))
 
 fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt
-    (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems))
+  (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems))
 
 end
 *}
diff -r 762ee71498fa -r b38a54bbfbd6 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CTT/CTT.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -380,21 +380,10 @@
 end
 *}
 
-method_setup form = {*
-  Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))
-*}
-
-method_setup typechk = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typechk_tac ctxt ths))
-*}
-
-method_setup intr = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intr_tac ctxt ths))
-*}
-
-method_setup equal = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (equal_tac ctxt ths))
-*}
+method_setup form = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt)) *}
+method_setup typechk = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typechk_tac ctxt ths)) *}
+method_setup intr = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intr_tac ctxt ths)) *}
+method_setup equal = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (equal_tac ctxt ths)) *}
 
 
 subsection {* Simplification *}
@@ -475,31 +464,16 @@
 fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms)
 *}
 
-method_setup eqintr = {*
-  Scan.succeed (SIMPLE_METHOD o eqintr_tac)
-*}
-
+method_setup eqintr = {* Scan.succeed (SIMPLE_METHOD o eqintr_tac) *}
 method_setup NE = {*
   Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s))
 *}
-
-method_setup pc = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))
-*}
-
-method_setup add_mp = {*
-  Scan.succeed (SIMPLE_METHOD' o add_mp_tac)
-*}
+method_setup pc = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths)) *}
+method_setup add_mp = {* Scan.succeed (SIMPLE_METHOD' o add_mp_tac) *}
 
 ML_file "rew.ML"
-
-method_setup rew = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))
-*}
-
-method_setup hyp_rew = {*
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))
-*}
+method_setup rew = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths)) *}
+method_setup hyp_rew = {* Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths)) *}
 
 
 subsection {* The elimination rules for fst/snd *}
diff -r 762ee71498fa -r b38a54bbfbd6 src/CTT/ex/Typechecking.thy
--- a/src/CTT/ex/Typechecking.thy	Tue Nov 11 13:44:09 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy	Tue Nov 11 13:50:56 2014 +0100
@@ -66,9 +66,7 @@
 
 (*Proofs involving arbitrary types.
   For concreteness, every type variable left over is forced to be N*)
-method_setup N = {*
-  Scan.succeed (fn _ => SIMPLE_METHOD (TRYALL (resolve_tac @{thms NF})))
-*}
+method_setup N = {* Scan.succeed (fn _ => SIMPLE_METHOD (TRYALL (resolve_tac @{thms NF}))) *}
 
 schematic_lemma "lam w. <w,w> : ?A"
 apply typechk