| changeset 36176 | 3fe7e97ccca8 |
| parent 34989 | b5c6e59e2cd7 |
| child 36866 | 426d5781bb25 |
--- a/src/FOL/FOL.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/FOL/FOL.thy Fri Apr 16 21:28:09 2010 +0200 @@ -371,7 +371,7 @@ lemmas induct_rulify_fallback = induct_forall_def induct_implies_def induct_equal_def induct_conj_def -hide const induct_forall induct_implies induct_equal induct_conj +hide_const induct_forall induct_implies induct_equal induct_conj text {* Method setup. *}