--- a/src/Pure/Isar/locale.ML Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/locale.ML Thu Apr 13 12:01:01 2006 +0200
@@ -1620,12 +1620,12 @@
val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
Tactic.rewrite_goals_tac [pred_def] THEN
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
+ Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
val conjuncts =
- (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
+ (Drule.equal_elim_rule2 OF [body_eq,
Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
- |> Drule.conj_elim_precise [length ts] |> hd;
+ |> Conjunction.elim_precise [length ts] |> hd;
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
prove_protected defs_thy t
(Tactic.rewrite_goals_tac defs THEN
--- a/src/Pure/Isar/proof.ML Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/proof.ML Thu Apr 13 12:01:01 2006 +0200
@@ -496,7 +496,7 @@
val _ = conditional (not (Pattern.matches thy
(Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
- in Drule.conj_elim_precise (map length propss) th end;
+ in Conjunction.elim_precise (map length propss) th end;
--- a/src/Pure/Isar/rule_cases.ML Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/rule_cases.ML Thu Apr 13 12:01:01 2006 +0200
@@ -195,7 +195,7 @@
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
else
Drule.fconv_rule
- (Drule.concl_conv ~1 (Drule.conjunction_conv ~1
+ (Drule.concl_conv ~1 (Conjunction.conv ~1
(K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
in
@@ -337,7 +337,7 @@
else
SOME (ns,
ths
- |> foldr1 (uncurry Drule.conj_intr)
+ |> foldr1 (uncurry Conjunction.intr)
|> Drule.implies_intr_list prems
|> Drule.standard'
|> save (hd raw_rules)
--- a/src/Pure/goal.ML Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/goal.ML Thu Apr 13 12:01:01 2006 +0200
@@ -147,7 +147,7 @@
val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
in
- hd (Drule.conj_elim_precise [length props] raw_result)
+ hd (Conjunction.elim_precise [length props] raw_result)
|> map
(Drule.implies_intr_list casms
#> Drule.forall_intr_list cparams
@@ -176,12 +176,12 @@
fun extract i n st =
(if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
else if n = 1 then Seq.single (Thm.cprem_of st i)
- else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
+ else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
|> Seq.map (Thm.adjust_maxidx #> init);
fun retrofit i n st' st =
(if n = 1 then st
- else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
+ else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
|> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
fun SELECT_GOAL tac i st =
--- a/src/Pure/tactic.ML Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/tactic.ML Thu Apr 13 12:01:01 2006 +0200
@@ -642,7 +642,7 @@
(* meta-level conjunction *)
val conj_tac = SUBGOAL (fn (goal, i) =>
- if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
+ if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
else no_tac);
val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
@@ -657,12 +657,12 @@
fun CONJUNCTS tac =
SELECT_GOAL (conjunction_tac 1
THEN tac
- THEN PRIMITIVE (Drule.conj_uncurry ~1));
+ THEN PRIMITIVE (Conjunction.uncurry ~1));
fun PRECISE_CONJUNCTS n tac =
SELECT_GOAL (precise_conjunction_tac n 1
THEN tac
- THEN PRIMITIVE (Drule.conj_uncurry ~1));
+ THEN PRIMITIVE (Conjunction.uncurry ~1));
end;