Mon, 04 Nov 2013 16:53:43 +0100 |
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
|
file | diff | annotate |
Wed, 18 Sep 2013 16:09:02 +0200 |
tuned proofs
|
file | diff | annotate |
Fri, 30 Aug 2013 12:43:39 +0200 |
tuned theory name
|
file | diff | annotate |
Fri, 30 Aug 2013 12:37:03 +0200 |
moved keywords down the hierarchy
|
file | diff | annotate |
Fri, 30 Aug 2013 12:12:41 +0200 |
renamed command to clarify connection with BNF
|
file | diff | annotate |
Fri, 30 Aug 2013 12:05:22 +0200 |
rationalized files
|
file | diff | annotate |
Thu, 08 Aug 2013 16:38:28 +0200 |
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
|
file | diff | annotate |
Thu, 25 Jul 2013 16:46:53 +0200 |
transfer rule for {c,d}tor_{,un}fold
|
file | diff | annotate |
Sat, 13 Jul 2013 13:03:21 +0200 |
got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
|
file | diff | annotate |
Thu, 11 Jul 2013 11:16:23 +0200 |
some new lemmas towards getting rid of in_bd BNF property; tuned
|
file | diff | annotate |
Wed, 01 May 2013 19:33:49 +0200 |
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
|
file | diff | annotate |
Mon, 29 Apr 2013 09:10:49 +0200 |
renamed BNF "(co)data" commands to names that are closer to their final names
|
file | diff | annotate |
Tue, 23 Apr 2013 11:43:09 +0200 |
(co)rec is (just as the (un)fold) the unique morphism;
|
file | diff | annotate |
Fri, 28 Sep 2012 09:12:50 +0200 |
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
|
file | diff | annotate |
Fri, 21 Sep 2012 18:25:17 +0200 |
tuned whitespace
|
file | diff | annotate |
Fri, 21 Sep 2012 16:45:06 +0200 |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file | diff | annotate | base |