equal
deleted
inserted
replaced
15 Pr=Standard_Prod and Su=Standard_Sum); |
15 Pr=Standard_Prod and Su=Standard_Sum); |
16 open Const Constructor; |
16 open Const Constructor; |
17 |
17 |
18 structure Inductive = Inductive_Fun |
18 structure Inductive = Inductive_Fun |
19 (val thy = con_thy; |
19 (val thy = con_thy; |
|
20 val thy_name = thy_name; |
20 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
21 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
21 val sintrs = sintrs; |
22 val sintrs = sintrs; |
22 val monos = monos; |
23 val monos = monos; |
23 val con_defs = con_defs; |
24 val con_defs = con_defs; |
24 val type_intrs = type_intrs; |
25 val type_intrs = type_intrs; |
36 Pr=Quine_Prod and Su=Quine_Sum); |
37 Pr=Quine_Prod and Su=Quine_Sum); |
37 open Const Constructor; |
38 open Const Constructor; |
38 |
39 |
39 structure CoInductive = CoInductive_Fun |
40 structure CoInductive = CoInductive_Fun |
40 (val thy = con_thy; |
41 (val thy = con_thy; |
|
42 val thy_name = thy_name; |
41 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
43 val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs); |
42 val sintrs = sintrs; |
44 val sintrs = sintrs; |
43 val monos = monos; |
45 val monos = monos; |
44 val con_defs = con_defs; |
46 val con_defs = con_defs; |
45 val type_intrs = type_intrs; |
47 val type_intrs = type_intrs; |