--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Dec 11 17:04:46 2008 +0100
@@ -361,7 +361,7 @@
| NONE => fn i => no_tac)
fun distinct_simproc names =
- Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"]
+ Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
(fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
case #context (#1 (rep_ss ss)) of
SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq])
--- a/src/HOL/Statespace/state_fun.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/state_fun.ML Thu Dec 11 17:04:46 2008 +0100
@@ -49,7 +49,7 @@
in
val lazy_conj_simproc =
- Simplifier.simproc HOL.thy "lazy_conj_simp" ["P & Q"]
+ Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
(fn thy => fn ss => fn t =>
(case t of (Const ("op &",_)$P$Q) =>
let
@@ -273,7 +273,7 @@
end;
in
val ex_lookup_eq_simproc =
- Simplifier.simproc HOL.thy "ex_lookup_eq_simproc" ["Ex t"]
+ Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
val ctxt = Simplifier.the_context ss |>
--- a/src/HOL/Statespace/state_space.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML Thu Dec 11 17:04:46 2008 +0100
@@ -230,7 +230,7 @@
| NONE => fn i => no_tac)
val distinct_simproc =
- Simplifier.simproc HOL.thy "StateSpace.distinct_simproc" ["x = y"]
+ Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
(fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
(case #context (#1 (rep_ss ss)) of
SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
--- a/src/HOL/Tools/TFL/dcterm.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Thu Dec 11 17:04:46 2008 +0100
@@ -74,7 +74,7 @@
* Some simple constructor functions.
*---------------------------------------------------------------------------*)
-val mk_hol_const = Thm.cterm_of HOL.thy o Const;
+val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
fun mk_exists (r as (Bvar, Body)) =
let val ty = #T(rep_cterm Bvar)
--- a/src/HOL/Tools/TFL/post.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/TFL/post.ML Thu Dec 11 17:04:46 2008 +0100
@@ -81,7 +81,7 @@
handle U.ERR _ => false;
-fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]);
val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
--- a/src/HOL/Tools/datatype_package.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -275,7 +275,7 @@
| distinct_proc _ _ _ = NONE;
val distinct_simproc =
- Simplifier.simproc HOL.thy distinctN ["s = t"] distinct_proc;
+ Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
val dist_ss = HOL_ss addsimprocs [distinct_simproc];
--- a/src/HOL/Tools/inductive_package.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -97,7 +97,7 @@
val notTrueE = TrueI RSN (2, notE);
val notFalseI = Seq.hd (atac 1 notI);
val simp_thms' = map (fn s => mk_meta_eq (the (find_first
- (equal (OldGoals.read_prop HOL.thy s) o prop_of) simp_thms)))
+ (equal (OldGoals.read_prop @{theory HOL} s) o prop_of) simp_thms)))
["(~True) = False", "(~False) = True",
"(True --> ?P) = ?P", "(False --> ?P) = True",
"(?P & True) = ?P", "(True & ?P) = ?P"];
@@ -410,7 +410,7 @@
local
(*delete needless equality assumptions*)
-val refl_thin = Goal.prove_global HOL.thy [] [] @{prop "!!P. a = a ==> P ==> P"}
+val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
(fn _ => assume_tac 1);
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
--- a/src/HOL/Tools/inductive_set_package.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -66,7 +66,7 @@
val anyt = Free ("t", TFree ("'t", []));
fun strong_ind_simproc tab =
- Simplifier.simproc_i HOL.thy "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+ Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
let
fun close p t f =
let val vs = Term.add_vars t []
@@ -317,7 +317,7 @@
fun to_pred_simproc rules =
let val rules' = map mk_meta_eq rules
in
- Simplifier.simproc_i HOL.thy "to_pred" [anyt]
+ Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
(fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
end;
--- a/src/HOL/Tools/record_package.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -858,7 +858,7 @@
if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
then Goal.prove (ProofContext.init thy) [] []
(Logic.list_implies (map Logic.varify asms,Logic.varify prop))
- (K (SkipProof.cheat_tac HOL.thy))
+ (K (SkipProof.cheat_tac @{theory HOL}))
(* standard can take quite a while for large records, thats why
* we varify the proposition manually here.*)
else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
@@ -924,7 +924,7 @@
* usual split rules for extensions can apply.
*)
val record_split_f_more_simproc =
- Simplifier.simproc HOL.thy "record_split_f_more_simp" ["x"]
+ Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
(trm as Abs _) =>
@@ -1000,7 +1000,7 @@
* subrecord.
*)
val record_simproc =
- Simplifier.simproc HOL.thy "record_simp" ["x"]
+ Simplifier.simproc @{theory HOL} "record_simp" ["x"]
(fn thy => fn ss => fn t =>
(case t of (sel as Const (s, Type (_,[domS,rangeS])))$
((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
@@ -1063,7 +1063,7 @@
* (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
*)
val record_upd_simproc =
- Simplifier.simproc HOL.thy "record_upd_simp" ["x"]
+ Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
(fn thy => fn ss => fn t =>
(case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
let datatype ('a,'b) calc = Init of 'b | Inter of 'a
@@ -1202,7 +1202,7 @@
*
*)
val record_eq_simproc =
- Simplifier.simproc HOL.thy "record_eq_simp" ["r = s"]
+ Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
(fn thy => fn _ => fn t =>
(case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
(case rec_id (~1) T of
@@ -1220,7 +1220,7 @@
* P t > 0: split up to given bound of record extensions
*)
fun record_split_simproc P =
- Simplifier.simproc HOL.thy "record_split_simp" ["x"]
+ Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
(fn thy => fn _ => fn t =>
(case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
@@ -1243,7 +1243,7 @@
| _ => NONE))
val record_ex_sel_eq_simproc =
- Simplifier.simproc HOL.thy "record_ex_sel_eq_simproc" ["Ex t"]
+ Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
(fn thy => fn ss => fn t =>
let
fun prove prop =
--- a/src/HOL/Tools/res_axioms.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Dec 11 17:04:46 2008 +0100
@@ -38,8 +38,8 @@
(**** Transformation of Elimination Rules into First-Order Formulas****)
-val cfalse = cterm_of HOL.thy HOLogic.false_const;
-val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
+val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
(*Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate the
@@ -47,9 +47,9 @@
fun transform_elim th =
case concl_of th of (*conclusion variable*)
Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
- Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
| v as Var(_, Type("prop",[])) =>
- Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
| _ => th;
(*To enforce single-threading*)
@@ -236,7 +236,7 @@
TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
(*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
+val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
(*cterm version of mk_cTrueprop*)
fun c_mkTrueprop A = Thm.capply cTrueprop A;
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Dec 11 17:04:46 2008 +0100
@@ -106,15 +106,9 @@
(* ----- general proofs ----------------------------------------------------- *)
-val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
- (fn prems =>[
- resolve_tac prems 1,
- cut_facts_tac prems 1,
- fast_tac HOL_cs 1]);
+val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
-val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y"
- (fn prems =>
- [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
+val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)}
in