author | berghofe |
Sun, 10 Jan 2010 18:41:07 +0100 | |
changeset 34914 | e391c3de0f6b |
parent 34913 | d8cb720c9c53 |
child 34915 | 7894c7dab132 |
src/FOL/FOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/FOL/FOL.thy Sun Jan 10 18:39:50 2010 +0100 +++ b/src/FOL/FOL.thy Sun Jan 10 18:41:07 2010 +0100 @@ -383,6 +383,8 @@ val atomize = @{thms induct_atomize} val rulify = @{thms induct_rulify} val rulify_fallback = @{thms induct_rulify_fallback} + fun dest_def _ = NONE + fun trivial_tac _ = no_tac ); *}