--- a/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 22:13:39 2008 +0200
@@ -308,7 +308,7 @@
\item [@{method rule_tac} etc.] do resolution of rules with explicit
instantiation. This works the same way as the ML tactics @{ML
- Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
+ res_inst_tac} etc. (see \cite[\S3]{isabelle-ref})
Multiple rules may be only given if there is no instantiation; then
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
@@ -323,12 +323,12 @@
\item [@{method thin_tac}~@{text \<phi>}] deletes the specified
assumption from a subgoal; note that @{text \<phi>} may contain schematic
- variables. See also @{ML Tactic.thin_tac} in
+ variables. See also @{ML thin_tac} in
\cite[\S3]{isabelle-ref}.
\item [@{method subgoal_tac}~@{text \<phi>}] adds @{text \<phi>} as an
- assumption to a subgoal. See also @{ML Tactic.subgoal_tac} and @{ML
- Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}.
+ assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
+ subgoals_tac} in \cite[\S3]{isabelle-ref}.
\item [@{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"}] renames
parameters of a goal according to the list @{text "x\<^sub>1, \<dots>,
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 22:13:39 2008 +0200
@@ -41,7 +41,7 @@
@{ML forward_tac}).
\item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
- @{ML RuleInsts.res_inst_tac}).
+ @{ML res_inst_tac}).
\item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
vs.\ @{ML rtac}).
@@ -66,11 +66,11 @@
\begin{tabular}{lll}
@{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
@{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
- @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
+ @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
@{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
@{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
@{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
- @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
+ @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
@{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
\end{tabular}
\medskip
--- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 22:13:39 2008 +0200
@@ -864,7 +864,7 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ (res_inst_tac (Simplifier.the_context ss)
[(("x", 1), "X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ss 1,
--- a/src/CCL/CCL.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/CCL.thy Mon Jun 16 22:13:39 2008 +0200
@@ -415,7 +415,7 @@
ML {*
fun po_coinduct_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
+ res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i
*}
@@ -460,11 +460,8 @@
done
ML {*
- fun eq_coinduct_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
-
- fun eq_coinduct3_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
+ fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i
+ fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i
*}
--- a/src/CCL/Hered.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/Hered.thy Mon Jun 16 22:13:39 2008 +0200
@@ -97,8 +97,7 @@
done
ML {*
- fun HTT_coinduct_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
+ fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i
*}
lemma HTT_coinduct3:
@@ -111,7 +110,7 @@
val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3}
fun HTT_coinduct3_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
+ res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
val HTTgenIs =
map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
--- a/src/CCL/Wfd.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CCL/Wfd.thy Mon Jun 16 22:13:39 2008 +0200
@@ -55,7 +55,7 @@
ML {*
fun wfd_strengthen_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
+ res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
*}
lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P"
@@ -456,7 +456,7 @@
in
fun rcall_tac ctxt i =
- let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i
+ let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
in IHinst tac @{thms rcallTs} i end
THEN eresolve_tac @{thms rcall_lemmas} i
@@ -478,7 +478,7 @@
hyp_subst_tac)
fun clean_ccs_tac ctxt =
- let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in
+ let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
hyp_subst_tac))
--- a/src/CTT/CTT.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CTT/CTT.thy Mon Jun 16 22:13:39 2008 +0200
@@ -417,13 +417,13 @@
The (rtac EqE i) lets them apply to equality judgements. **)
fun NE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
fun SumE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
fun PlusE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
--- a/src/FOL/FOL.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/FOL/FOL.thy Mon Jun 16 22:13:39 2008 +0200
@@ -70,8 +70,7 @@
done
ML {*
- fun case_tac ctxt a =
- RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
+ fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
*}
method_setup case_tac =
--- a/src/HOL/Auth/Message.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Auth/Message.thy Mon Jun 16 22:13:39 2008 +0200
@@ -884,8 +884,7 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (RuleInsts.res_inst_tac (Simplifier.the_context ss)
- [(("x", 1), "X")] (insert_commute RS ssubst) 1),
+ (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ss 1,
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Bali/Basis.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Jun 16 22:13:39 2008 +0200
@@ -230,7 +230,7 @@
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
- (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+ (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
--- a/src/HOL/Bali/WellType.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Bali/WellType.thy Mon Jun 16 22:13:39 2008 +0200
@@ -653,10 +653,11 @@
apply (safe del: disjE)
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i =>
- if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
- RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
- RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
- else RuleInsts.thin_tac @{context} "All ?P" i) *})
+ if i = 11 then EVERY'
+ [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
+ thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
+ thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
+ else thin_tac @{context} "All ?P" i) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*})
apply (simp_all (no_asm_use) split del: split_if_asm)
--- a/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 22:13:39 2008 +0200
@@ -50,7 +50,7 @@
fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
resolve_tac @{thms deriv_rulesI} i ORELSE
- ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)]
+ ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
@{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
--- a/src/HOL/IMPP/Hoare.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/IMPP/Hoare.thy Mon Jun 16 22:13:39 2008 +0200
@@ -283,7 +283,7 @@
apply (blast) (* cut *)
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
- [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y",
+ [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
--- a/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 22:13:39 2008 +0200
@@ -108,8 +108,8 @@
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
-apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *})
-apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 22:13:39 2008 +0200
@@ -54,7 +54,7 @@
gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
fun cut_inst_tac_term' tinst th =
- res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
+ res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
fun get_dyn_thm thy name atom_name =
PureThy.get_thm thy name handle ERROR _ =>
--- a/src/HOL/Prolog/prolog.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Prolog/prolog.ML Mon Jun 16 22:13:39 2008 +0200
@@ -53,7 +53,7 @@
fun atomizeD ctxt thm = let
fun at thm = case concl_of thm of
_$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
- (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
+ (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
| _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const("op -->",_)$_$_) => at(thm RS mp)
| _ => [thm]
--- a/src/HOL/Real/rat_arith.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Real/rat_arith.ML Mon Jun 16 22:13:39 2008 +0200
@@ -14,7 +14,7 @@
val simps =
[@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
- RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
+ read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
@{thm divide_1}, @{thm divide_zero_left},
@{thm times_divide_eq_right}, @{thm times_divide_eq_left},
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
--- a/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 22:13:39 2008 +0200
@@ -880,7 +880,7 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ (res_inst_tac (Simplifier.the_context ss)
[(("x", 1), "X")] (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ss 1,
--- a/src/HOL/TLA/TLA.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/TLA/TLA.thy Mon Jun 16 22:13:39 2008 +0200
@@ -307,15 +307,15 @@
fun merge_temp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
- RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
+ eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i])
fun merge_stp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
- RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
+ eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i])
fun merge_act_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
- RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
+ eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
*}
(* rewrite rule to push universal quantification through box:
--- a/src/HOL/Tools/TFL/post.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/TFL/post.ML Mon Jun 16 22:13:39 2008 +0200
@@ -152,7 +152,7 @@
rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE)));
(*Strip off the outer !P*)
-val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
+val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec;
fun tracing true _ = ()
| tracing false msg = writeln msg;
--- a/src/HOL/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200
@@ -44,7 +44,7 @@
(case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
Var (xi, _) :: _ => xi
| _ => raise THM ("Malformed cases rule", 0, [rule]));
- in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end
+ in res_inst_tac ctxt [(xi, s)] rule i st end
handle THM _ => Seq.empty;
fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
@@ -100,7 +100,7 @@
val concls = HOLogic.dest_concls (Thm.concl_of rule);
val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
error "Induction rule has different numbers of variables";
- in RuleInsts.res_inst_tac ctxt insts rule i st end
+ in res_inst_tac ctxt insts rule i st end
handle THM _ => Seq.empty;
end;
--- a/src/HOL/Tools/meson.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jun 16 22:13:39 2008 +0200
@@ -646,7 +646,7 @@
(*Rules to convert the head literal into a negated assumption. If the head
literal is already negated, then using notEfalse instead of notEfalse'
prevents a double negation.*)
-val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE;
+val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE;
val notEfalse' = rotate_prems 1 notEfalse;
fun negated_asm_of_head th =
--- a/src/HOL/Tools/metis_tools.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML Mon Jun 16 22:13:39 2008 +0200
@@ -24,10 +24,10 @@
(* ------------------------------------------------------------------------- *)
(* Useful Theorems *)
(* ------------------------------------------------------------------------- *)
- val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE);
+ val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE);
val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*)
val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE);
- val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
+ val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em);
(* ------------------------------------------------------------------------- *)
(* Useful Functions *)
--- a/src/HOL/Tools/record_package.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/record_package.ML Mon Jun 16 22:13:39 2008 +0200
@@ -2155,8 +2155,8 @@
fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} =>
fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
- st |> (RuleInsts.res_inst_tac context [((rN, 0), s)] cases_scheme 1
- THEN RuleInsts.res_inst_tac context [((rN, 0), s')] cases_scheme 1
+ st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
+ THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
THEN (METAHYPS equality_tac 1))
(* simp_all_tac ss (sel_convs) would also work but is less efficient *)
end);
--- a/src/HOL/Tools/split_rule.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML Mon Jun 16 22:13:39 2008 +0200
@@ -124,7 +124,7 @@
fun pair_tac ctxt s =
- RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+ res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
THEN' hyp_subst_tac
THEN' K prune_params_tac;
--- a/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 22:13:39 2008 +0200
@@ -41,9 +41,9 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
- RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ res_inst_tac (Simplifier.the_context ss)
[(("act", 0), sact)] @{thm totalize_transientI} 2
- ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
+ ORELSE res_inst_tac (Simplifier.the_context ss)
[(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm Domain_def}]) 3,
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 22:13:39 2008 +0200
@@ -1089,7 +1089,7 @@
ML {*
fun Seq_case_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
+ res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
@@ -1104,7 +1104,7 @@
(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac ctxt s rws i =
let val ss = Simplifier.local_simpset_of ctxt in
- RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
THEN simp_tac (ss addsimps rws) i
end;
@@ -1114,13 +1114,13 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
fun pair_tac ctxt s =
- RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE
+ res_inst_tac ctxt [(("p", 0), s)] PairE
THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
(* induction on a sequence of pairs with pairsplitting and simplification *)
fun pair_induct_tac ctxt s rws i =
let val ss = Simplifier.local_simpset_of ctxt in
- RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
THEN pair_tac ctxt "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
THEN simp_tac (ss addsimps rws) i
--- a/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 22:13:39 2008 +0200
@@ -24,7 +24,7 @@
fun upd_second f (x,y,z) = ( x, f y, z);
fun upd_third f (x,y,z) = ( x, y, f z);
-fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt;
+fun atomize ctxt thm = let val r_inst = read_instantiate ctxt;
fun at thm = case concl_of thm of
_$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 22:13:39 2008 +0200
@@ -376,7 +376,7 @@
val goal = lift_defined %: (nonlazy args, concl);
fun tacs ctxt = [
rtac @{thm rev_contrapos} 1,
- RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
+ eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
in
@@ -477,7 +477,7 @@
mk_trp (con_app con1 args1 ~<< con_app con2 args2));
fun tacs ctxt = [
rtac @{thm rev_contrapos} 1,
- RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
+ eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
@ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
@ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
@@ -709,7 +709,7 @@
mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
val take_ss = HOL_ss addsimps take_rews;
fun quant_tac ctxt i = EVERY
- (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
+ (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
fun ind_prems_tac prems = EVERY
(maps (fn cons =>
@@ -766,7 +766,7 @@
map (K (atac 1)) (nonlazy args) @
map (K (etac spec 1)) (List.filter is_rec args);
fun cases_tacs (cons, cases) =
- RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 ::
+ res_inst_tac context [(("x", 0), "x")] cases 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
maps con_tacs cons;
in
@@ -783,8 +783,8 @@
val concl = mk_trp (%:(x_name n) === %:(x_name n^"'"));
val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl;
fun tacf {prems, context} = [
- RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
- RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
+ res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1,
+ res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1,
stac fix_def2 1,
REPEAT (CHANGED
(rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)),
@@ -833,7 +833,7 @@
val goal =
mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
fun arg_tacs ctxt vn = [
- RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
+ eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
etac disjE 1,
asm_simp_tac (HOL_ss addsimps con_rews) 1,
asm_simp_tac take_ss 1];
@@ -843,7 +843,7 @@
fun foo_tacs ctxt n (cons, cases) =
simp_tac take_ss 1 ::
rtac allI 1 ::
- RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
+ res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
asm_simp_tac take_ss 1 ::
maps (con_tacs ctxt) cons;
fun tacs ctxt =
@@ -887,8 +887,7 @@
else (* infinite case *)
let
fun one_finite n dn =
- RuleInsts.read_instantiate global_ctxt
- [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
+ read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
val finites = mapn one_finite 1 dnames;
val goal =
@@ -936,7 +935,7 @@
fun x_tacs ctxt n x = [
rotate_tac (n+1) 1,
etac all2E 1,
- RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+ eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
TRY (safe_tac HOL_cs),
REPEAT (CHANGED (asm_simp_tac take_ss 1))];
fun tacs ctxt = [
--- a/src/LCF/LCF.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/LCF/LCF.thy Mon Jun 16 22:13:39 2008 +0200
@@ -317,7 +317,7 @@
ML {*
fun induct_tac ctxt v i =
- RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
+ res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
REPEAT (resolve_tac @{thms adm_lemmas} i)
*}
@@ -376,7 +376,7 @@
ML {*
fun induct2_tac ctxt (f, g) i =
- RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
+ res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN
REPEAT(resolve_tac @{thms adm_lemmas} i)
*}
--- a/src/Sequents/LK0.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/Sequents/LK0.thy Mon Jun 16 22:13:39 2008 +0200
@@ -157,11 +157,11 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
+ res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
fun cutL_tac ctxt s i =
- RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
+ res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
*}
--- a/src/ZF/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200
@@ -102,7 +102,7 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state
+ eres_inst_tac ctxt [(ixn, var)] rule i state
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
--- a/src/ZF/UNITY/SubstAx.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Mon Jun 16 22:13:39 2008 +0200
@@ -360,7 +360,7 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
- RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
+ res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
--- a/src/ZF/ind_syntax.ML Mon Jun 16 17:56:08 2008 +0200
+++ b/src/ZF/ind_syntax.ML Mon Jun 16 22:13:39 2008 +0200
@@ -51,7 +51,7 @@
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
val equals_CollectD =
- RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
+ read_instantiate @{context} [(("W", 0), "?Q")]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));