| changeset 49309 | f20b24214ac2 |
| parent 49308 | 6190b701e4f4 |
| child 49312 | c874ff5658dc |
| 49308:6190b701e4f4 | 49309:f20b24214ac2 |
|---|---|
10 theory BNF_LFP |
10 theory BNF_LFP |
11 imports BNF_FP |
11 imports BNF_FP |
12 keywords |
12 keywords |
13 "data_raw" :: thy_decl and |
13 "data_raw" :: thy_decl and |
14 "data" :: thy_decl |
14 "data" :: thy_decl |
15 uses |
|
16 "Tools/bnf_lfp_util.ML" |
|
17 "Tools/bnf_lfp_tactics.ML" |
|
18 "Tools/bnf_lfp.ML" |
|
19 begin |
15 begin |
20 |
16 |
17 ML_file "Tools/bnf_lfp_util.ML" |
|
18 ML_file "Tools/bnf_lfp_tactics.ML" |
|
19 ML_file "Tools/bnf_lfp.ML" |
|
20 |
|
21 end |
21 end |