equal
deleted
inserted
replaced
4 |
4 |
5 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} |
5 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} |
6 |
6 |
7 theory Inductive |
7 theory Inductive |
8 imports Complete_Lattices |
8 imports Complete_Lattices |
|
9 keywords "monos" |
9 uses |
10 uses |
10 "Tools/dseq.ML" |
11 "Tools/dseq.ML" |
11 ("Tools/inductive.ML") |
12 ("Tools/inductive.ML") |
12 ("Tools/Datatype/datatype_aux.ML") |
13 ("Tools/Datatype/datatype_aux.ML") |
13 ("Tools/Datatype/datatype_prop.ML") |
14 ("Tools/Datatype/datatype_prop.ML") |