# HG changeset patch # User wenzelm # Date 1005592943 -3600 # Node ID a5cf3ea0685d458920d6c429246629a7686a6abe # Parent b3a708ddedf870d42ee3afdeef10a0181c840c92 val local_imp_def = thm "induct_implies_def"; diff -r b3a708ddedf8 -r a5cf3ea0685d src/FOL/FOL.thy --- 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";