# HG changeset patch
# User wenzelm
# Date 1267564819 -3600
# Node ID d4e747d3a87472ab21e7bd4e414b3eb2c7e91445
# Parent  08c37d7bd2ad6179ac98e52d2eeff9c9b377bd7d
standard convention for syntax consts;

diff -r 08c37d7bd2ad -r d4e747d3a874 src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Tue Mar 02 22:18:51 2010 +0100
+++ b/src/ZF/List_ZF.thy	Tue Mar 02 22:20:19 2010 +0100
@@ -15,8 +15,8 @@
 
 
 syntax
- "[]"        :: i                                       ("[]")
- "_List"     :: "is => i"                                 ("[(_)]")
+ "_Nil" :: i  ("[]")
+ "_List" :: "is => i"  ("[(_)]")
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"