| Tue, 19 Nov 2013 14:11:26 +0100 |
blanchet |
use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package
|
file |
diff |
annotate
|
| Wed, 13 Nov 2013 11:23:25 +0100 |
traytel |
tuned example
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 13:29:04 +0200 |
traytel |
use new coinduction method and primcorec in examples
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:56:15 +0200 |
blanchet |
use singular to avoid confusion
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 16:10:58 +0200 |
traytel |
tuned example
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 18:22:55 +0200 |
traytel |
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
remove unnecessary dependencies on Library/Quotient_*
|
file |
diff |
annotate
|
| Mon, 29 Apr 2013 09:10:49 +0200 |
blanchet |
renamed BNF "(co)data" commands to names that are closer to their final names
|
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 |
export "dtor_map_coinduct" theorems, since they're used in one example
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
adapted examples to new names
|
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
|