--- a/src/HOL/Induct/SList.thy Mon Jun 04 15:43:30 2007 +0200
+++ b/src/HOL/Induct/SList.thy Mon Jun 04 15:43:31 2007 +0200
@@ -24,7 +24,9 @@
Tidied by lcp. Still needs removal of nat_rec.
*)
-theory SList imports Sexp begin
+theory SList
+imports Sexp
+begin
(*Hilbert_Choice is needed for the function "inv"*)
@@ -77,12 +79,12 @@
(*Declaring the abstract list constructors*)
-no_translations
+(*<*)no_translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
no_syntax
Nil :: "'a list" ("[]")
- Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "#" 65)
+ Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "#" 65)(*>*)
definition
Nil :: "'a list" ("[]") where
@@ -159,10 +161,8 @@
map :: "('a=>'b) => ('a list => 'b list)" where
"map f xs = list_rec xs [] (%x l r. f(x)#r)"
-no_syntax
- append :: "'a list => 'a list => 'a list" (infixr "@" 65)
-hide const "List.append"
-
+(*<*)no_syntax
+ "\<^const>List.append" :: "'a list => 'a list => 'a list" (infixr "@" 65)(*>*)
definition
append :: "['a list, 'a list] => 'a list" (infixr "@" 65) where
"xs@ys = list_rec xs ys (%x l r. x#r)"
@@ -230,8 +230,6 @@
enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"
-no_syntax
- "@" :: "'a list => 'a list => 'a list" (infixr 65)
no_translations
"[x:xs . P]" == "filter (%x. P) xs"