# HG changeset patch
# User haftmann
# Date 1162826914 -3600
# Node ID 25a5ab43a5ffa4b0d8fcdcd2cb030de5307395e7
# Parent  5fe5cd5fede7ed54362afbd889d16791e1d63916
removed itrev as inlining theorem

diff -r 5fe5cd5fede7 -r 25a5ab43a5ff src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 06 16:28:33 2006 +0100
+++ b/src/HOL/List.thy	Mon Nov 06 16:28:34 2006 +0100
@@ -2816,7 +2816,7 @@
 lemmas list_bex_code [code unfold] =
   list_ex_iff [symmetric, THEN eq_reflection]
 
-lemma itrev [simp, normal post]:
+lemma itrev [simp]:
   "itrev xs ys = rev xs @ ys"
   by (induct xs arbitrary: ys) simp_all
 
@@ -2828,7 +2828,7 @@
   "map_filter f P xs = map f (filter P xs)"
   by (induct xs) auto
 
-lemma rev_code [code func, code unfold]:
+lemma rev_code [code func, code unfold, code noinline]:
   "rev xs == itrev xs []"
   by simp