equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
8 header {* Least Fixed Point Operation on Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_LFP |
10 theory BNF_LFP |
11 imports BNF_Comp |
11 imports BNF_FP |
12 keywords |
12 keywords |
13 "data_raw" :: thy_decl |
13 "data_raw" :: thy_decl and |
|
14 "data" :: thy_decl |
14 uses |
15 uses |
15 "Tools/bnf_lfp_util.ML" |
16 "Tools/bnf_lfp_util.ML" |
16 "Tools/bnf_lfp_tactics.ML" |
17 "Tools/bnf_lfp_tactics.ML" |
17 "Tools/bnf_lfp.ML" |
18 "Tools/bnf_lfp.ML" |
18 begin |
19 begin |