Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/BNF/Tools/bnf_gfp.ML
2012-10-12
wenzelm
2012-10-12
discontinued typedef with alternative name;
file
|
diff
|
annotate
2012-10-12
wenzelm
2012-10-12
discontinued typedef with implicit set_def;
file
|
diff
|
annotate
2012-09-30
blanchet
2012-09-30
tuning
file
|
diff
|
annotate
2012-09-28
blanchet
2012-09-28
renamed ML file in preparation for next step
file
|
diff
|
annotate
2012-09-28
blanchet
2012-09-28
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
file
|
diff
|
annotate
2012-09-27
traytel
2012-09-27
type of the bound of a BNF depends at most on dead type variables
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
tweaked theorem names (in particular, dropped s's)
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
fixed "rels" + split them into injectivity and distinctness
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
generate high-level "coinduct" and "strong_coinduct" properties
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
export "dtor_map_coinduct" theorems, since they're used in one example
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
generate high-level "maps", "sets", and "rels" properties
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
use singular since there is always only one theorem
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
file
|
diff
|
annotate
2012-09-26
blanchet
2012-09-26
leave out some internal theorems unless "bnf_note_all" is set
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
renamed coinduction principles to have "dtor" in the name
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
renamed "map_simps" to "{c,d}tor_maps"
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
simplified fact policies
file
|
diff
|
annotate
2012-09-23
blanchet
2012-09-23
started work on generation of "rel" theorems
file
|
diff
|
annotate
2012-09-21
blanchet
2012-09-21
renamed LFP low-level rel property to have ctor not dtor in its name
file
|
diff
|
annotate
2012-09-21
blanchet
2012-09-21
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
file
|
diff
|
annotate
2012-09-21
blanchet
2012-09-21
fixed a few names that escaped the renaming
file
|
diff
|
annotate
2012-09-21
blanchet
2012-09-21
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
file
|
diff
|
annotate
|
base