src/HOL/Induct/PropLog.ML

 qed "imp_false";
 
 (*This formulation is required for strong induction hypotheses*)
 Goal "hyps p tt |- (if tt[p] then p else p->false)";
 by (rtac (split_if RS iffD2) 1);
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
 by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
 			      weaken_right, imp_false]
                        addSEs [false_imp]) 1);
 qed "hyps_thms_if";

 (*** Completeness -- lemmas for reducing the set of assumptions ***)
 
 (*For the case hyps(p,t)-insert(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
   we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
 Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_insert";
 
 (** Two lemmas for use with weaken_left **)

 by (induct_tac "p" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "hyps_finite";
 
 Goal "hyps p t <= (UN v. {#v, #v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed "hyps_subset";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;