src/ZF/ex/Acc.thy
changeset 809 1daa0269eb5d
parent 578 efc648d29dd0
child 1401 0c439768f45c
--- a/src/ZF/ex/Acc.thy	Mon Dec 19 15:17:29 1994 +0100
+++ b/src/ZF/ex/Acc.thy	Mon Dec 19 15:22:42 1994 +0100
@@ -9,7 +9,7 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = WF + "Inductive" +
+Acc = WF + Inductive +
 
 consts
   acc :: "i=>i"