| 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 10:59:10 +0200 |
blanchet |
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:01:00 +0200 |
blanchet |
got rid of other instance of shaky "Thm.generalize"
|
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:01:00 +0200 |
blanchet |
get rid of shaky "Thm.generalize"
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:01:00 +0200 |
blanchet |
fixed "rels" + split them into injectivity and distinctness
|
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 |
added coinduction tactic
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "maps", "sets", and "rels" properties
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
nicer type var names
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
took out accidentally submitted "tracing" calls
|
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 19:17:49 +0200 |
blanchet |
renamed LFP low-level rel property to have ctor not dtor in its name
|
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
|