--- a/src/HOL/ex/NormalForm.thy Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy Thu Sep 25 10:17:22 2008 +0200
@@ -8,15 +8,6 @@
imports Main "~~/src/HOL/Real/Rational"
begin
-lemma [code nbe]:
- "x = x \<longleftrightarrow> True" by rule+
-
-lemma [code nbe]:
- "eq_class.eq (x::bool) x \<longleftrightarrow> True" unfolding eq by rule+
-
-lemma [code nbe]:
- "eq_class.eq (x::nat) x \<longleftrightarrow> True" unfolding eq by rule+
-
lemma "True" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code nbe]
@@ -29,9 +20,6 @@
datatype n = Z | S n
-lemma [code nbe]:
- "eq_class.eq (x::n) x \<longleftrightarrow> True" unfolding eq by rule+
-
consts
add :: "n \<Rightarrow> n \<Rightarrow> n"
add2 :: "n \<Rightarrow> n \<Rightarrow> n"
@@ -83,9 +71,6 @@
lemma "[] @ xs = xs" by normalization
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
-lemma [code nbe]:
- "eq_class.eq (x :: 'a\<Colon>eq list) x \<longleftrightarrow> True" unfolding eq by rule+
-
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
lemma "rev [a, b, c] = [c, b, a]" by normalization
normal_form "rev (a#b#cs) = rev cs @ [b, a]"