src/FOL/FOL.thy
changeset 34914 e391c3de0f6b
parent 32960 69916a850301
child 34989 b5c6e59e2cd7
     1.1 --- a/src/FOL/FOL.thy	Sun Jan 10 18:39:50 2010 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sun Jan 10 18:41:07 2010 +0100
     1.3 @@ -383,6 +383,8 @@
     1.4      val atomize = @{thms induct_atomize}
     1.5      val rulify = @{thms induct_rulify}
     1.6      val rulify_fallback = @{thms induct_rulify_fallback}
     1.7 +    fun dest_def _ = NONE
     1.8 +    fun trivial_tac _ = no_tac
     1.9    );
    1.10  *}
    1.11