src/ZF/ex/Acc.thy

--- a/src/ZF/ex/Acc.thy	Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/ex/Acc.thy	Thu Aug 25 12:09:21 1994 +0200
@@ -9,10 +9,10 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = WF + "inductive" +
+Acc = WF + "Inductive" +
 
 consts
-  "acc" :: "i=>i"
+  acc :: "i=>i"
 
 inductive
   domains "acc(r)" <= "field(r)"