| author | blanchet |
| Wed, 12 Sep 2012 05:21:47 +0200 | |
| changeset 49309 | f20b24214ac2 |
| parent 49308 | 6190b701e4f4 |
| child 49312 | c874ff5658dc |
| permissions | -rw-r--r-- |
|
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Codatatype/BNF_FP.thy |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
5 |
|
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
6 |
Composition of bounded natural functors. |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
7 |
*) |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
8 |
|
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
9 |
header {* Composition of Bounded Natural Functors *}
|
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
10 |
|
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
11 |
theory BNF_FP |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
12 |
imports BNF_Comp BNF_Wrap |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
13 |
keywords |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
14 |
"defaults" |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
15 |
begin |
|
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
16 |
|
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
17 |
ML_file "Tools/bnf_fp_util.ML" |
|
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
18 |
ML_file "Tools/bnf_fp_sugar_tactics.ML" |
|
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
19 |
ML_file "Tools/bnf_fp_sugar.ML" |
|
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
20 |
|
|
49308
6190b701e4f4
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet
parents:
diff
changeset
|
21 |
end |