changeset 12160 | a5cf3ea0685d |
parent 12127 | 219e543496a3 |
child 12164 | 0b219d9e3384 |
--- a/src/FOL/FOL.thy Mon Nov 12 12:38:40 2001 +0100 +++ b/src/FOL/FOL.thy Mon Nov 12 20:22:23 2001 +0100 @@ -75,6 +75,7 @@ (struct val dest_concls = FOLogic.dest_concls; val cases_default = thm "case_split"; + val local_imp_def = thm "induct_implies_def"; val local_impI = thm "induct_impliesI"; val conjI = thm "conjI"; val atomize = thms "induct_atomize";