Wed, 27 Nov 2013 15:08:18 +0100 |
traytel |
command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
|
file |
diff |
annotate
|
Wed, 20 Nov 2013 20:45:20 +0100 |
blanchet |
moved 'coinduction' proof method to 'HOL'
|
file |
diff |
annotate
|
Wed, 20 Nov 2013 20:18:53 +0100 |
blanchet |
move registration of countable set type as BNF to its own theory file (+ renamed theory)
|
file |
diff |
annotate
|
Wed, 02 Oct 2013 11:57:52 +0200 |
traytel |
new coinduction method
|
file |
diff |
annotate
|
Wed, 21 Aug 2013 10:58:15 +0200 |
traytel |
tuned theory imports
|
file |
diff |
annotate
|
Thu, 25 Jul 2013 16:46:53 +0200 |
traytel |
transfer rule for {c,d}tor_{,un}fold
|
file |
diff |
annotate
|
Mon, 22 Jul 2013 21:12:15 +0200 |
traytel |
transfer rule for map (not yet registered as a transfer rule)
|
file |
diff |
annotate
|
Tue, 07 May 2013 18:40:23 +0200 |
traytel |
removed dead internal constants/theorems
|
file |
diff |
annotate
|
Tue, 07 May 2013 14:47:22 +0200 |
traytel |
tuned
|
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
|