| Wed, 13 Nov 2013 10:53:36 +0100 |
traytel |
more explicit syntax for defining a bnf
|
file |
diff |
annotate
|
| Tue, 22 Oct 2013 16:07:09 +0200 |
traytel |
removed junk
|
file |
diff |
annotate
|
| Tue, 22 Oct 2013 14:17:12 +0200 |
traytel |
define a trivial nonemptiness witness if none is provided
|
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
|
| Mon, 15 Jul 2013 15:50:39 +0200 |
traytel |
killed unused theorems
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 13:03:21 +0200 |
traytel |
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 10:24:00 +0200 |
traytel |
Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
|
file |
diff |
annotate
|
| Tue, 07 May 2013 14:22:54 +0200 |
traytel |
got rid of the set based relator---use (binary) predicate based relator instead
|
file |
diff |
annotate
|
| Tue, 30 Apr 2013 13:34:31 +0200 |
blanchet |
renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 19:18:20 +0200 |
traytel |
removed unnecessary assumptions in some theorems about cardinal exponentiation
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 11:05:33 +0100 |
traytel |
hide internal constants; tuned proofs
|
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
|