--- a/src/HOL/Induct/SList.thy Wed May 19 11:41:58 2004 +0200
+++ b/src/HOL/Induct/SList.thy Fri May 21 21:14:18 2004 +0200
@@ -90,6 +90,7 @@
(* list Enumeration *)
consts
"[]" :: "'a list" ("[]")
+syntax
"@list" :: "args => 'a list" ("[(_)]")
translations