equal
deleted
inserted
replaced
10 "inductive" "coinductive" :: thy_decl and |
10 "inductive" "coinductive" :: thy_decl and |
11 "inductive_cases" "inductive_simps" :: thy_script and "monos" and |
11 "inductive_cases" "inductive_simps" :: thy_script and "monos" and |
12 "rep_datatype" :: thy_goal and |
12 "rep_datatype" :: thy_goal and |
13 "primrec" :: thy_decl |
13 "primrec" :: thy_decl |
14 uses |
14 uses |
15 "Tools/dseq.ML" |
|
16 ("Tools/inductive.ML") |
15 ("Tools/inductive.ML") |
17 ("Tools/Datatype/datatype_aux.ML") |
16 ("Tools/Datatype/datatype_aux.ML") |
18 ("Tools/Datatype/datatype_prop.ML") |
17 ("Tools/Datatype/datatype_prop.ML") |
19 ("Tools/Datatype/datatype_data.ML") |
18 ("Tools/Datatype/datatype_data.ML") |
20 ("Tools/Datatype/datatype_case.ML") |
19 ("Tools/Datatype/datatype_case.ML") |