--- a/src/HOL/List.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/List.thy Tue Oct 31 09:28:56 2006 +0100
@@ -2651,19 +2651,19 @@
code_type list
(SML "_ list")
- (Haskell target_atom "[_]")
+ (Haskell "![_]")
code_const Nil
- (SML target_atom "[]")
- (Haskell target_atom "[]")
+ (SML "[]")
+ (Haskell "[]")
code_type char
- (SML target_atom "char")
- (Haskell target_atom "Char")
+ (SML "char")
+ (Haskell "Char")
code_const Char
- (SML target_atom "(__,/ __)")
- (Haskell target_atom "(__,/ __)")
+ (SML "!(__,/ __)")
+ (Haskell "!(__,/ __)")
code_instance list :: eq and char :: eq
(Haskell - and -)
@@ -2815,7 +2815,7 @@
lemmas list_bex_code [code unfold] =
list_ex_iff [symmetric, THEN eq_reflection]
-lemma itrev [simp]:
+lemma itrev [simp, normal post]:
"itrev xs ys = rev xs @ ys"
by (induct xs arbitrary: ys) simp_all
@@ -2831,7 +2831,4 @@
"rev xs == itrev xs []"
by simp
-lemmas itrev_rev [normal post] =
- rev_code [symmetric]
-
end