# HG changeset patch # User wenzelm # Date 1237565557 -3600 # Node ID 983e8b6e4e6910784872aeb499db28b52221af5f # Parent d9805c5b5d2ef44ab6e4d4126bd80be322a5b11e Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory; diff -r d9805c5b5d2e -r 983e8b6e4e69 NEWS --- 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 \ ... \; additional antiquotation forms: diff -r d9805c5b5d2e -r 983e8b6e4e69 src/FOL/blastdata.ML --- 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; diff -r d9805c5b5d2e -r 983e8b6e4e69 src/FOL/simpdata.ML --- 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 ***) diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOL/HOL.thy --- 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; *} diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOL/Tools/simpdata.ML --- 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 *) diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/FOCUS/Buffer.thy --- 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; diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/IOA/Modelcheck/Cockpit.thy --- 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 diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/IOA/Modelcheck/MuIOA.thy --- 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); diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy --- 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)]); diff -r d9805c5b5d2e -r 983e8b6e4e69 src/HOLCF/IOA/Modelcheck/Ring3.thy --- 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 diff -r d9805c5b5d2e -r 983e8b6e4e69 src/Provers/blast.ML --- 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; diff -r d9805c5b5d2e -r 983e8b6e4e69 src/Provers/clasimp.ML --- 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 *) diff -r d9805c5b5d2e -r 983e8b6e4e69 src/Provers/classical.ML --- 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" #> diff -r d9805c5b5d2e -r 983e8b6e4e69 src/Provers/splitter.ML --- 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 *) diff -r d9805c5b5d2e -r 983e8b6e4e69 src/Pure/simplifier.ML --- 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 *) diff -r d9805c5b5d2e -r 983e8b6e4e69 src/ZF/Tools/inductive_package.ML --- 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;