author | berghofe |
Sat, 30 Jan 2010 17:01:01 +0100 | |
changeset 34989 | b5c6e59e2cd7 |
parent 34988 | cca208c8d619 |
child 34990 | 81e8fdfeb849 |
src/FOL/FOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/FOL/FOL.thy Sat Jan 30 16:59:49 2010 +0100 +++ b/src/FOL/FOL.thy Sat Jan 30 17:01:01 2010 +0100 @@ -383,6 +383,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 _ = NONE fun trivial_tac _ = no_tac );