changeset 34991 | 1adaefa63c5a |
parent 34974 | 18b41bba42b5 |
parent 34988 | cca208c8d619 |
child 35115 | 446c5063e4fd |
--- a/src/HOL/HOL.thy Thu Jan 28 11:48:49 2010 +0100 +++ b/src/HOL/HOL.thy Sun Jan 31 15:22:40 2010 +0100 @@ -1453,6 +1453,7 @@ val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify'} val rulify_fallback = @{thms induct_rulify_fallback} + val equal_def = @{thm induct_equal_def} fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u) | dest_def _ = NONE val trivial_tac = match_tac @{thms induct_trueI}