--- a/src/FOL/blastdata.ML Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/blastdata.ML Sat Mar 15 22:07:26 2008 +0100
@@ -1,14 +1,12 @@
-
-val ccontr = thm "ccontr";
(*** Applying BlastFun to create Blast_tac ***)
structure Blast_Data =
struct
type claset = Cla.claset
- val equality_name = "op ="
- val not_name = "Not"
- val notE = notE
- val ccontr = ccontr
+ val equality_name = @{const_name "op ="}
+ val not_name = @{const_name Not}
+ val notE = @{thm notE}
+ val ccontr = @{thm ccontr}
val contr_tac = Cla.contr_tac
val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
--- a/src/FOL/cladata.ML Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/cladata.ML Sat Mar 15 22:07:26 2008 +0100
@@ -11,9 +11,9 @@
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
- val mp = mp
- val not_elim = notE
- val classical = thm "classical"
+ val mp = @{thm mp}
+ val not_elim = @{thm notE}
+ val classical = @{thm classical}
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
end;
@@ -27,12 +27,13 @@
(*Propositional rules*)
val prop_cs = empty_cs
- addSIs [refl, TrueI, conjI, thm "disjCI", impI, notI, iffI]
- addSEs [conjE, disjE, thm "impCE", FalseE, thm "iffCE"];
+ addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI},
+ @{thm notI}, @{thm iffI}]
+ addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffCE}];
(*Quantifier rules*)
-val FOL_cs = prop_cs addSIs [allI, thm "ex_ex1I"] addIs [exI]
- addSEs [exE, thm "alt_ex1E"] addEs [allE];
+val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
+ addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
--- a/src/FOL/ex/Prolog.thy Sat Mar 15 22:07:25 2008 +0100
+++ b/src/FOL/ex/Prolog.thy Sat Mar 15 22:07:26 2008 +0100
@@ -63,7 +63,7 @@
(*backtracking version*)
ML {*
-val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)
+val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1)
*}
lemma "rev(?x, a:b:c:Nil)"
@@ -76,13 +76,13 @@
(*rev([a..p], ?w) requires 153 inferences *)
lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
-apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
done
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences
total inferences = 2 + 1 + 17 + 561 = 581*)
lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
-apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
+apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
done
end
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 15 22:07:26 2008 +0100
@@ -469,7 +469,7 @@
(*some risk of excessive simplification here -- might have
to identify the bare minimum set of rewrites*)
full_simp_tac
- (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
+ (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN
--- a/src/ZF/Tools/typechk.ML Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/Tools/typechk.ML Sat Mar 15 22:07:26 2008 +0100
@@ -93,8 +93,8 @@
fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
(*Compiles a term-net for speed*)
-val basic_res_tac = net_resolve_tac [TrueI,refl,reflexive_thm,iff_refl,
- @{thm ballI},allI,conjI,impI];
+val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
+ @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
(*Instantiates variables in typing conditions.
drawback: does not simplify conjunctions*)
--- a/src/ZF/arith_data.ML Sat Mar 15 22:07:25 2008 +0100
+++ b/src/ZF/arith_data.ML Sat Mar 15 22:07:26 2008 +0100
@@ -130,7 +130,7 @@
fun simplify_meta_eq rules =
let val ss0 =
FOL_ss addeqcongs [@{thm eq_cong2}, @{thm iff_cong2}]
- delsimps iff_simps (*these could erase the whole rule!*)
+ delsimps @{thms iff_simps} (*these could erase the whole rule!*)
addsimps rules
in fn ss => mk_meta_eq o simplify (Simplifier.inherit_context ss ss0) end;