isabelle: File revisions

src/HOL/BNF/BNF_LFP.thy

2013-11-04	blanchet	2013-11-04	split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')	file \| diff \| annotate
2013-09-18	traytel	2013-09-18	tuned proofs	file \| diff \| annotate
2013-08-30	blanchet	2013-08-30	tuned theory name	file \| diff \| annotate
2013-08-30	blanchet	2013-08-30	moved keywords down the hierarchy	file \| diff \| annotate
2013-08-30	blanchet	2013-08-30	renamed command to clarify connection with BNF	file \| diff \| annotate
2013-08-30	blanchet	2013-08-30	rationalized files	file \| diff \| annotate
2013-08-08	traytel	2013-08-08	theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map	file \| diff \| annotate
2013-07-25	traytel	2013-07-25	transfer rule for {c,d}tor_{,un}fold	file \| diff \| annotate
2013-07-13	traytel	2013-07-13	got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)	file \| diff \| annotate
2013-07-11	traytel	2013-07-11	some new lemmas towards getting rid of in_bd BNF property; tuned	file \| diff \| annotate
2013-05-01	blanchet	2013-05-01	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
2013-04-29	blanchet	2013-04-29	renamed BNF "(co)data" commands to names that are closer to their final names	file \| diff \| annotate
2013-04-23	traytel	2013-04-23	(co)rec is (just as the (un)fold) the unique morphism;	file \| diff \| annotate
2012-09-28	blanchet	2012-09-28	killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"	file \| diff \| annotate
2012-09-21	blanchet	2012-09-21	tuned whitespace	file \| diff \| annotate
2012-09-21	blanchet	2012-09-21	renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"	file \| diff \| annotate \| base

isabelle

RSS Atom