src/HOL/HOL.thy
changeset 12240 0760eda193c4
parent 12161 ea4fbf26a945
child 12256 26243ebf2831
     1.1 --- a/src/HOL/HOL.thy	Mon Nov 19 17:42:00 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 19 20:46:05 2001 +0100
     1.3 @@ -321,12 +321,12 @@
     1.4    (struct
     1.5      val dest_concls = HOLogic.dest_concls;
     1.6      val cases_default = thm "case_split";
     1.7 -    val local_imp_def = thm "induct_implies_def";
     1.8      val local_impI = thm "induct_impliesI";
     1.9      val conjI = thm "conjI";
    1.10      val atomize = thms "induct_atomize";
    1.11      val rulify1 = thms "induct_rulify1";
    1.12      val rulify2 = thms "induct_rulify2";
    1.13 +    val localize = [Thm.symmetric (thm "induct_implies_def")];
    1.14    end);
    1.15  *}
    1.16