tuned
authorhaftmann
Fri Apr 20 17:58:24 2007 +0200 (2007-04-20)
changeset 22758a7790c8e3c14
parent 22757 d3298d63b7b6
child 22759 e4a3f49eb924
tuned
src/HOL/Code_Generator.thy
     1.1 --- a/src/HOL/Code_Generator.thy	Fri Apr 20 16:55:38 2007 +0200
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Apr 20 17:58:24 2007 +0200
     1.3 @@ -164,14 +164,6 @@
     1.4  code_datatype "TYPE('a)"
     1.5  
     1.6  
     1.7 -text {* prevent unfolding of quantifier definitions *}
     1.8 -
     1.9 -lemma [code func]:
    1.10 -  "Ex = Ex"
    1.11 -  "All = All"
    1.12 -  by rule+
    1.13 -
    1.14 -
    1.15  text {* code generation for undefined as exception *}
    1.16  
    1.17  code_const undefined