# HG changeset patch
# User lcp
# Date 787839898 -3600
# Node ID 6330ca0a3ac54325c4caff500fd5483e035d38a9
# Parent  96f51689cdeb7ef65bb03bedd12db24355f3cf1a
removed quotes around "Inductive"

diff -r 96f51689cdeb -r 6330ca0a3ac5 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Mon Dec 19 13:18:54 1994 +0100
+++ b/src/ZF/Finite.thy	Mon Dec 19 13:24:58 1994 +0100
@@ -6,7 +6,7 @@
 Finite powerset operator
 *)
 
-Finite = Arith + "Inductive" +
+Finite = Arith + Inductive +
 consts
   Fin 	    :: "i=>i"
   FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
diff -r 96f51689cdeb -r 6330ca0a3ac5 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Mon Dec 19 13:18:54 1994 +0100
+++ b/src/ZF/Zorn.thy	Mon Dec 19 13:24:58 1994 +0100
@@ -11,7 +11,7 @@
 Union_in_Pow is proved in ZF.ML
 *)
 
-Zorn = OrderArith + AC + "Inductive" +
+Zorn = OrderArith + AC + Inductive +
 
 consts
   Subset_rel      :: "i=>i"