equal
deleted
inserted
replaced
11 |
11 |
12 header{*Inductive and Coinductive Definitions*} |
12 header{*Inductive and Coinductive Definitions*} |
13 |
13 |
14 theory Inductive_ZF |
14 theory Inductive_ZF |
15 imports Fixedpt QPair Nat_ZF |
15 imports Fixedpt QPair Nat_ZF |
|
16 keywords |
|
17 "elimination" "induction" "case_eqns" "recursor_eqns" |
|
18 "domains" "intros" "monos" "con_defs" "type_intros" "type_elims" |
16 uses |
19 uses |
17 ("ind_syntax.ML") |
20 ("ind_syntax.ML") |
18 ("Tools/cartprod.ML") |
21 ("Tools/cartprod.ML") |
19 ("Tools/ind_cases.ML") |
22 ("Tools/ind_cases.ML") |
20 ("Tools/inductive_package.ML") |
23 ("Tools/inductive_package.ML") |