# HG changeset patch
# User lcp
# Date 787846962 -3600
# Node ID 1daa0269eb5d46cbe2af165b247e414a9011cb98
# Parent  c51c1f59e59ebd32e1e9e30cce715192a9232ddb
removed quotes around "Inductive"

diff -r c51c1f59e59e -r 1daa0269eb5d src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Mon Dec 19 15:17:29 1994 +0100
+++ b/src/ZF/Datatype.thy	Mon Dec 19 15:22:42 1994 +0100
@@ -1,5 +1,5 @@
 (*Dummy theory to document dependencies *)
 
-Datatype = "constructor" + "Inductive" + Univ + QUniv
+Datatype = "constructor" + Inductive + Univ + QUniv
 
-(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
+(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
diff -r c51c1f59e59e -r 1daa0269eb5d src/ZF/ex/Acc.thy
--- 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"