Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed quotes around "Inductive"
authorlcp
Mon, 19 Dec 1994 13:24:58 +0100
changeset 806 6330ca0a3ac5
parent 805 96f51689cdeb
child 807 3abd026e68a4
removed quotes around "Inductive"
src/ZF/Finite.thy file | annotate | diff | comparison | revisions
src/ZF/Zorn.thy file | annotate | diff | comparison | revisions 
--- 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)
--- 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"
isabelle