src/HOL/Code_Setup.thy
changeset 24844 98c006a30218
parent 24835 8c26128f8997
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Oct 04 19:46:09 2007 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:54:44 2007 +0200
     1.3 @@ -127,11 +127,6 @@
     1.4  
     1.5  lemmas [code func] = Let_def if_True if_False
     1.6  
     1.7 -setup {*
     1.8 -  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
     1.9 -  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
    1.10 -*}
    1.11 -
    1.12  
    1.13  subsection {* Evaluation oracle *}
    1.14  
    1.15 @@ -160,5 +155,4 @@
    1.16        THEN' resolve_tac [TrueI, refl]))
    1.17  *} "solve goal by normalization"
    1.18  
    1.19 -
    1.20  end