equal
deleted
inserted
replaced
14 Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j)) |
14 Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j)) |
15 Fin(univ(A)) <= univ(A) |
15 Fin(univ(A)) <= univ(A) |
16 *) |
16 *) |
17 |
17 |
18 structure Fin = Inductive_Fun |
18 structure Fin = Inductive_Fun |
19 (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] |
19 (val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)] |
20 val rec_doms = [("Fin","Pow(A)")] |
20 val rec_doms = [("Fin","Pow(A)")] |
21 val sintrs = ["0 : Fin(A)", |
21 val sintrs = ["0 : Fin(A)", |
22 "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] |
22 "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] |
23 val monos = [] |
23 val monos = [] |
24 val con_defs = [] |
24 val con_defs = [] |