Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Finite.thy
changeset 578 efc648d29dd0
parent 534 cd8bec47e175
child 806 6330ca0a3ac5 
--- a/src/ZF/Finite.thy	Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Finite.thy	Thu Aug 25 12:09:21 1994 +0200
@@ -6,7 +6,7 @@
 Finite powerset operator
 *)
 
-Finite = Arith + 
+Finite = Arith + "Inductive" +
 consts
   Fin 	    :: "i=>i"
   FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
isabelle