# HG changeset patch
# User wenzelm
# Date 750085872 -3600
# Node ID eb7ad4a7dc4fe0cf8a5aec708c1f7d44c91ee088
# Parent  d981488bda7b541d25ce07e0e8c0d461717c0e91
@List: replaced "args" by "is";

diff -r d981488bda7b -r eb7ad4a7dc4f src/ZF/ListFn.thy
--- a/src/ZF/ListFn.thy	Fri Oct 08 13:55:04 1993 +0100
+++ b/src/ZF/ListFn.thy	Fri Oct 08 14:11:12 1993 +0100
@@ -23,7 +23,7 @@
 
  (* List Enumeration *)
  "[]"        :: "i" 	                           	("[]")
- "@List"     :: "args => i" 	                   	("[(_)]")
+ "@List"     :: "is => i" 	                   	("[(_)]")
 
 
 translations
diff -r d981488bda7b -r eb7ad4a7dc4f src/ZF/listfn.thy
--- a/src/ZF/listfn.thy	Fri Oct 08 13:55:04 1993 +0100
+++ b/src/ZF/listfn.thy	Fri Oct 08 14:11:12 1993 +0100
@@ -23,7 +23,7 @@
 
  (* List Enumeration *)
  "[]"        :: "i" 	                           	("[]")
- "@List"     :: "args => i" 	                   	("[(_)]")
+ "@List"     :: "is => i" 	                   	("[(_)]")
 
 
 translations