--- 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 =
--- 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 {*
--- 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 *}
--- 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 ***)
--- 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
*}
--- 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 *}
--- 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