# HG changeset patch
# User haftmann
# Date 1177084704 -7200
# Node ID a7790c8e3c14a5e777ed4b7615a6f03cbce42b58
# Parent  d3298d63b7b663065f321629a4cf41f56a5185e5
tuned

diff -r d3298d63b7b6 -r a7790c8e3c14 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Fri Apr 20 16:55:38 2007 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Apr 20 17:58:24 2007 +0200
@@ -164,14 +164,6 @@
 code_datatype "TYPE('a)"
 
 
-text {* prevent unfolding of quantifier definitions *}
-
-lemma [code func]:
-  "Ex = Ex"
-  "All = All"
-  by rule+
-
-
 text {* code generation for undefined as exception *}
 
 code_const undefined