| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
compatibility option to use "rep_datatype"
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 18:39:17 +0200 |
blanchet |
use a nicer scheme to indexify names
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 17:54:35 +0200 |
blanchet |
repaired signature
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 17:00:54 +0200 |
blanchet |
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:01:00 +0200 |
blanchet |
tweaked theorem names (in particular, dropped s's)
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "coinduct" and "strong_coinduct" properties
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
parameterized "subst_tac"
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "maps", "sets", and "rels" properties
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
started work on generation of "rel" theorems
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:45:06 +0200 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
| base
|