--- a/src/ZF/fin.ML Thu Mar 17 11:24:31 1994 +0100
+++ b/src/ZF/fin.ML Thu Mar 17 12:36:58 1994 +0100
@@ -18,13 +18,12 @@
*)
structure Fin = Inductive_Fun
- (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
- val rec_doms = [("Fin","Pow(A)")];
- val sintrs =
- ["0 : Fin(A)",
- "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
- val monos = [];
- val con_defs = [];
+ (val thy = Arith.thy addconsts [(["Fin"],"i=>i")]
+ val rec_doms = [("Fin","Pow(A)")]
+ val sintrs = ["0 : Fin(A)",
+ "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
+ val monos = []
+ val con_defs = []
val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);