| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
rationalized dependencies
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved hide_const from BNF to Main
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
moved BNF files to 'HOL'
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 21:22:01 +0100 |
blanchet |
hide short const name
|
file |
diff |
annotate
|
| Wed, 18 Dec 2013 11:03:40 +0100 |
traytel |
express weak pullback property of bnfs only in terms of the relator
|
file |
diff |
annotate
|
| 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
|