src/HOL/Codatatype/Examples/Misc_Data.thy
2012-09-21 blanchet 2012-09-21 renamed top-level theory from "Codatatype" to "BNF"
2012-09-20 blanchet 2012-09-20 provide predicator, define relator
2012-09-20 blanchet 2012-09-20 adapting "More_BNFs" to new relators/predicators
2012-09-20 blanchet 2012-09-20 adapted FP code to new relator approach
2012-09-20 blanchet 2012-09-20 adapted BNF composition to new relator approach
2012-09-18 blanchet 2012-09-18 further tuned simpset
2012-09-08 blanchet 2012-09-08 repaired "nofail4" example
2012-09-06 traytel 2012-09-06 handle type constructors not known to be a BNF using the DEADID BNF
2012-09-06 traytel 2012-09-06 respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-05 blanchet 2012-09-05 adapted example
2012-09-05 blanchet 2012-09-05 commented out slow examples again
2012-09-05 blanchet 2012-09-05 ported "Misc_Codata" to new syntax
2012-09-05 blanchet 2012-09-05 ported "Misc_Data" to new syntax
2012-09-04 blanchet 2012-09-04 removed oddities
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands
2012-08-28 blanchet 2012-08-28 fixed import paths in examples
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)