Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
--- a/NEWS Fri Mar 20 17:04:44 2009 +0100
+++ b/NEWS Fri Mar 20 17:12:37 2009 +0100
@@ -685,6 +685,12 @@
Syntax.read_term_global etc.; see also OldGoals.read_term as last
resort for legacy applications.
+* Disposed old declarations, tactics, tactic combinators that refer to
+the simpset or claset of an implicit theory (such as Addsimps,
+Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in
+embedded ML text, or local_simpset_of with a proper context passed as
+explicit runtime argument.
+
* Antiquotations: block-structured compilation context indicated by
\<lbrace> ... \<rbrace>; additional antiquotation forms:
--- a/src/FOL/blastdata.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/FOL/blastdata.ML Fri Mar 20 17:12:37 2009 +0100
@@ -1,5 +1,5 @@
-(*** Applying BlastFun to create Blast_tac ***)
+(*** Applying BlastFun to create blast_tac ***)
structure Blast_Data =
struct
type claset = Cla.claset
@@ -10,13 +10,10 @@
val contr_tac = Cla.contr_tac
val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
- val claset = Cla.claset
- val rep_cs = Cla.rep_cs
+ val rep_cs = Cla.rep_cs
val cla_modifiers = Cla.cla_modifiers;
val cla_meth' = Cla.cla_meth'
end;
structure Blast = BlastFun(Blast_Data);
-
-val Blast_tac = Blast.Blast_tac
-and blast_tac = Blast.blast_tac;
+val blast_tac = Blast.blast_tac;
--- a/src/FOL/simpdata.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/FOL/simpdata.ML Fri Mar 20 17:12:37 2009 +0100
@@ -117,8 +117,6 @@
val split_asm_tac = Splitter.split_asm_tac;
val op addsplits = Splitter.addsplits;
val op delsplits = Splitter.delsplits;
-val Addsplits = Splitter.Addsplits;
-val Delsplits = Splitter.Delsplits;
(*** Standard simpsets ***)
--- a/src/HOL/HOL.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOL/HOL.thy Fri Mar 20 17:12:37 2009 +0100
@@ -1018,12 +1018,10 @@
val contr_tac = Classical.contr_tac
val dup_intr = Classical.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
- val claset = Classical.claset
val rep_cs = Classical.rep_cs
val cla_modifiers = Classical.cla_modifiers
val cla_meth' = Classical.cla_meth'
);
-val Blast_tac = Blast.Blast_tac;
val blast_tac = Blast.blast_tac;
*}
--- a/src/HOL/Tools/simpdata.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOL/Tools/simpdata.ML Fri Mar 20 17:12:37 2009 +0100
@@ -147,8 +147,6 @@
val op addsplits = Splitter.addsplits;
val op delsplits = Splitter.delsplits;
-val Addsplits = Splitter.Addsplits;
-val Delsplits = Splitter.Delsplits;
(* integration of simplifier with classical reasoner *)
--- a/src/HOLCF/FOCUS/Buffer.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Fri Mar 20 17:12:37 2009 +0100
@@ -98,8 +98,11 @@
by (erule subst, rule refl)
ML {*
-fun B_prover s tac eqs = prove_goal (the_context ()) s (fn prems => [cut_facts_tac prems 1,
- tac 1, auto_tac (claset(), simpset() addsimps eqs)]);
+fun B_prover s tac eqs =
+ let val thy = the_context () in
+ prove_goal thy s (fn prems => [cut_facts_tac prems 1,
+ tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
+ end;
fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Mar 20 17:12:37 2009 +0100
@@ -102,18 +102,18 @@
(* to prove, that info is always set at the recent alarm *)
lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm arrives (and after each acknowledgment),
info remains at None *)
lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm would be acknowledged, it must be arrived *)
lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
apply auto
done
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Fri Mar 20 17:12:37 2009 +0100
@@ -278,14 +278,14 @@
by (REPEAT (rtac impI 1));
by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs)
+by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
delsimps [not_iff,split_part])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
by (full_simp_tac
(Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
by (REPEAT (if_full_simp_tac
- (simpset() delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+ (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Fri Mar 20 17:12:37 2009 +0100
@@ -18,18 +18,18 @@
(* is_sim_tac makes additionally to call_sim_tac some simplifications,
which are suitable for implementation realtion formulas *)
-fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
+fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) =>
EVERY [REPEAT (etac thin_rl i),
- simp_tac (simpset() addsimps [ioa_implements_def]) i,
+ simp_tac (ss addsimps [ioa_implements_def]) i,
rtac conjI i,
rtac conjI (i+1),
TRY(call_sim_tac thm_list (i+2)),
TRY(atac (i+2)),
REPEAT(rtac refl (i+2)),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i+1),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i)]);
--- a/src/HOLCF/IOA/Modelcheck/Ring3.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Ring3.thy Fri Mar 20 17:12:37 2009 +0100
@@ -114,7 +114,7 @@
(* property to prove: at most one (of 3) members of the ring will
declare itself to leader *)
lemma at_most_one_leader: "ring =<| one_leader"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
apply auto
done
--- a/src/Provers/blast.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/Provers/blast.ML Fri Mar 20 17:12:37 2009 +0100
@@ -48,7 +48,6 @@
val contr_tac : int -> tactic
val dup_intr : thm -> thm
val hyp_subst_tac : bool -> int -> tactic
- val claset : unit -> claset
val rep_cs : (* dependent on classical.ML *)
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
@@ -77,7 +76,6 @@
val depth_tac : claset -> int -> int -> tactic
val depth_limit : int Config.T
val blast_tac : claset -> int -> tactic
- val Blast_tac : int -> tactic
val setup : theory -> theory
(*debugging tools*)
val stats : bool ref
@@ -89,7 +87,7 @@
val instVars : term -> (unit -> unit)
val toTerm : int -> term -> Term.term
val readGoal : theory -> string -> term
- val tryInThy : theory -> int -> string ->
+ val tryInThy : theory -> claset -> int -> string ->
(int->tactic) list * branch list list * (int*int*exn) list
val normBr : branch -> branch
end;
@@ -1283,7 +1281,6 @@
((if !trace then warning ("blast: " ^ s) else ());
Seq.empty);
-fun Blast_tac i = blast_tac (Data.claset()) i;
(*** For debugging: these apply the prover to a subgoal and return
@@ -1294,11 +1291,11 @@
(*Read a string to make an initial, singleton branch*)
fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal;
-fun tryInThy thy lim s =
+fun tryInThy thy cs lim s =
let
val state as State {fullTrace = ft, ...} = initialize thy;
val res = timeap prove
- (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I);
+ (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I);
val _ = fullTrace := !ft;
in res end;
--- a/src/Provers/clasimp.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/Provers/clasimp.ML Fri Mar 20 17:12:37 2009 +0100
@@ -26,8 +26,6 @@
type clasimpset
val get_css: Context.generic -> clasimpset
val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
- val change_clasimpset: (clasimpset -> clasimpset) -> unit
- val clasimpset: unit -> clasimpset
val local_clasimpset_of: Proof.context -> clasimpset
val addSIs2: clasimpset * thm list -> clasimpset
val addSEs2: clasimpset * thm list -> clasimpset
@@ -42,19 +40,10 @@
val addss': claset * simpset -> claset
val addIffs: clasimpset * thm list -> clasimpset
val delIffs: clasimpset * thm list -> clasimpset
- val AddIffs: thm list -> unit
- val DelIffs: thm list -> unit
- val CLASIMPSET: (clasimpset -> tactic) -> tactic
- val CLASIMPSET': (clasimpset -> 'a -> tactic) -> 'a -> tactic
val clarsimp_tac: clasimpset -> int -> tactic
- val Clarsimp_tac: int -> tactic
val mk_auto_tac: clasimpset -> int -> int -> tactic
val auto_tac: clasimpset -> tactic
- val Auto_tac: tactic
- val auto: unit -> unit
val force_tac: clasimpset -> int -> tactic
- val Force_tac: int -> tactic
- val force: int -> unit
val fast_simp_tac: clasimpset -> int -> tactic
val slow_simp_tac: clasimpset -> int -> tactic
val best_simp_tac: clasimpset -> int -> tactic
@@ -84,9 +73,6 @@
let val (cs', ss') = f (get_css context)
in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
-fun change_clasimpset f = Context.>> (fn context => (Context.the_theory context; map_css f context));
-fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
-
fun local_clasimpset_of ctxt =
(Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
@@ -168,9 +154,6 @@
Simplifier.addsimps);
val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
-fun AddIffs thms = change_clasimpset (fn css => css addIffs thms);
-fun DelIffs thms = change_clasimpset (fn css => css delIffs thms);
-
fun addIffs_generic (x, ths) =
Library.foldl (addIff (addXEs, addXIs) (addXEs, addXIs) #1) ((x, ()), ths) |> #1;
@@ -182,19 +165,10 @@
(* tacticals *)
-fun CLASIMPSET tacf state =
- Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss))) state;
-
-fun CLASIMPSET' tacf i state =
- Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
-
-
fun clarsimp_tac (cs, ss) =
safe_asm_full_simp_tac ss THEN_ALL_NEW
Classical.clarify_tac (cs addSss ss);
-fun Clarsimp_tac i = clarsimp_tac (clasimpset ()) i;
-
(* auto_tac *)
@@ -231,8 +205,6 @@
end;
fun auto_tac css = mk_auto_tac css 4 2;
-fun Auto_tac st = auto_tac (clasimpset ()) st;
-fun auto () = by Auto_tac;
(* force_tac *)
@@ -242,8 +214,6 @@
Classical.clarify_tac cs' 1,
IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
ALLGOALS (Classical.first_best_tac cs')]) end;
-fun Force_tac i = force_tac (clasimpset ()) i;
-fun force i = by (Force_tac i);
(* basic combinations *)
--- a/src/Provers/classical.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/Provers/classical.ML Fri Mar 20 17:12:37 2009 +0100
@@ -69,11 +69,7 @@
val appSWrappers : claset -> wrapper
val appWrappers : claset -> wrapper
- val change_claset: (claset -> claset) -> unit
val claset_of: theory -> claset
- val claset: unit -> claset
- val CLASET: (claset -> tactic) -> tactic
- val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic
val local_claset_of : Proof.context -> claset
val fast_tac : claset -> int -> tactic
@@ -107,24 +103,6 @@
val inst_step_tac : claset -> int -> tactic
val inst0_step_tac : claset -> int -> tactic
val instp_step_tac : claset -> int -> tactic
-
- val AddDs : thm list -> unit
- val AddEs : thm list -> unit
- val AddIs : thm list -> unit
- val AddSDs : thm list -> unit
- val AddSEs : thm list -> unit
- val AddSIs : thm list -> unit
- val Delrules : thm list -> unit
- val Safe_tac : tactic
- val Safe_step_tac : int -> tactic
- val Clarify_tac : int -> tactic
- val Clarify_step_tac : int -> tactic
- val Step_tac : int -> tactic
- val Fast_tac : int -> tactic
- val Best_tac : int -> tactic
- val Slow_tac : int -> tactic
- val Slow_best_tac : int -> tactic
- val Deepen_tac : int -> int -> tactic
end;
signature CLASSICAL =
@@ -870,23 +848,9 @@
fun map_context_cs f = GlobalClaset.map (apsnd
(fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-fun change_claset f = Context.>> (Context.map_theory (map_claset f));
-
fun claset_of thy =
let val (cs, ctxt_cs) = GlobalClaset.get thy
in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
-val claset = claset_of o ML_Context.the_global_context;
-
-fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
-fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
-
-fun AddDs args = change_claset (fn cs => cs addDs args);
-fun AddEs args = change_claset (fn cs => cs addEs args);
-fun AddIs args = change_claset (fn cs => cs addIs args);
-fun AddSDs args = change_claset (fn cs => cs addSDs args);
-fun AddSEs args = change_claset (fn cs => cs addSEs args);
-fun AddSIs args = change_claset (fn cs => cs addSIs args);
-fun Delrules args = change_claset (fn cs => cs delrules args);
(* context dependent components *)
@@ -930,21 +894,6 @@
val rule_del = attrib delrule o ContextRules.rule_del;
-(* tactics referring to the implicit claset *)
-
-(*the abstraction over the proof state delays the dereferencing*)
-fun Safe_tac st = safe_tac (claset()) st;
-fun Safe_step_tac i st = safe_step_tac (claset()) i st;
-fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
-fun Clarify_tac i st = clarify_tac (claset()) i st;
-fun Step_tac i st = step_tac (claset()) i st;
-fun Fast_tac i st = fast_tac (claset()) i st;
-fun Best_tac i st = best_tac (claset()) i st;
-fun Slow_tac i st = slow_tac (claset()) i st;
-fun Slow_best_tac i st = slow_best_tac (claset()) i st;
-fun Deepen_tac m = deepen_tac (claset()) m;
-
-
end;
@@ -972,15 +921,12 @@
(** proof methods **)
-fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
-fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
-
-
local
-fun some_rule_tac ctxt (CS {xtra_netpair, ...}) facts = SUBGOAL (fn (goal, i) =>
+fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
let
val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
+ val CS {xtra_netpair, ...} = local_claset_of ctxt;
val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
@@ -990,16 +936,15 @@
end)
THEN_ALL_NEW Goal.norm_hhf_tac;
-fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
- | rule_tac rules _ _ facts = Method.rule_tac rules facts;
+in
-fun default_tac rules ctxt cs facts =
- HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
+fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
+ | rule_tac _ rules facts = Method.rule_tac rules facts;
+
+fun default_tac ctxt rules facts =
+ HEADGOAL (rule_tac ctxt rules facts) ORELSE
Class.default_intro_tac ctxt facts;
-in
- val rule = METHOD_CLASET' o rule_tac;
- val default = METHOD_CLASET o default_tac;
end;
@@ -1033,9 +978,11 @@
(** setup_methods **)
val setup_methods =
- Method.setup @{binding default} (Attrib.thms >> default)
+ Method.setup @{binding default}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
- Method.setup @{binding rule} (Attrib.thms >> rule)
+ Method.setup @{binding rule}
+ (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
"apply some intro/elim rule (potentially classical)" #>
Method.setup @{binding contradiction} (Scan.succeed (K contradiction))
"proof by contradiction" #>
--- a/src/Provers/splitter.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/Provers/splitter.ML Fri Mar 20 17:12:37 2009 +0100
@@ -35,8 +35,6 @@
val split_asm_tac : thm list -> int -> tactic
val addsplits : simpset * thm list -> simpset
val delsplits : simpset * thm list -> simpset
- val Addsplits : thm list -> unit
- val Delsplits : thm list -> unit
val split_add: attribute
val split_del: attribute
val split_modifiers : Method.modifier parser list
@@ -453,9 +451,6 @@
in Simplifier.delloop (ss, split_name name asm)
end in Library.foldl delsplit (ss,splits) end;
-fun Addsplits splits = (change_simpset (fn ss => ss addsplits splits));
-fun Delsplits splits = (change_simpset (fn ss => ss delsplits splits));
-
(* attributes *)
--- a/src/Pure/simplifier.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/Pure/simplifier.ML Fri Mar 20 17:12:37 2009 +0100
@@ -10,15 +10,8 @@
include BASIC_META_SIMPLIFIER
val change_simpset: (simpset -> simpset) -> unit
val simpset_of: theory -> simpset
- val simpset: unit -> simpset
- val SIMPSET: (simpset -> tactic) -> tactic
- val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
- val Addsimps: thm list -> unit
- val Delsimps: thm list -> unit
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
- val Addcongs: thm list -> unit
- val Delcongs: thm list -> unit
val local_simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
@@ -27,11 +20,6 @@
val full_simp_tac: simpset -> int -> tactic
val asm_lr_simp_tac: simpset -> int -> tactic
val asm_full_simp_tac: simpset -> int -> tactic
- val Simp_tac: int -> tactic
- val Asm_simp_tac: int -> tactic
- val Full_simp_tac: int -> tactic
- val Asm_lr_simp_tac: int -> tactic
- val Asm_full_simp_tac: int -> tactic
val simplify: simpset -> thm -> thm
val asm_simplify: simpset -> thm -> thm
val full_simplify: simpset -> thm -> thm
@@ -138,17 +126,9 @@
fun map_simpset f = Context.theory_map (map_ss f);
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
-val simpset = simpset_of o ML_Context.the_global_context;
-fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
-fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
-
-fun Addsimps args = change_simpset (fn ss => ss addsimps args);
-fun Delsimps args = change_simpset (fn ss => ss delsimps args);
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
-fun Addcongs args = change_simpset (fn ss => ss addcongs args);
-fun Delcongs args = change_simpset (fn ss => ss delcongs args);
(* local simpset *)
@@ -283,13 +263,6 @@
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
-(*the abstraction over the proof state delays the dereferencing*)
-fun Simp_tac i st = simp_tac (simpset ()) i st;
-fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st;
-fun Full_simp_tac i st = full_simp_tac (simpset ()) i st;
-fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st;
-fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
-
(* conversions *)
--- a/src/ZF/Tools/inductive_package.ML Fri Mar 20 17:04:44 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Fri Mar 20 17:12:37 2009 +0100
@@ -16,7 +16,6 @@
dom_subset : thm, (*inclusion of recursive set in dom*)
intrs : thm list, (*introduction rules*)
elim : thm, (*case analysis theorem*)
- mk_cases : string -> thm, (*generates case theorems*)
induct : thm, (*main induction rule*)
mutual_induct : thm}; (*mutual induction rule*)
@@ -275,9 +274,6 @@
(basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
(Thm.assume A RS elim)
|> Drule.standard';
- fun mk_cases a = make_cases (*delayed evaluation of body!*)
- (simpset ())
- let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
fun induction_rules raw_induct thy =
let
@@ -548,7 +544,6 @@
dom_subset = dom_subset',
intrs = intrs'',
elim = elim',
- mk_cases = mk_cases,
induct = induct,
mutual_induct = mutual_induct})
end;