src/HOL/Library/FinFun.thy
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2015-06-26 wenzelm 2015-06-26 tuned proofs;
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-08 Andreas Lochbihler 2013-08-08 prefer Code.abort with explicit error message
2013-05-15 kuncar 2013-05-15 superfluous transfer rule
2013-02-14 Andreas Lochbihler 2013-02-14 instantiate finite_UNIV and card_UNIV for finfun type
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-06-12 Andreas Lochbihler 2012-06-12 add lemma to FinFun
2012-06-04 Andreas Lochbihler 2012-06-04 more sort constraints for FinFun code generation
2012-06-01 Andreas Lochbihler 2012-06-01 simplify card_UNIV type class, tuned proofs
2012-05-31 Andreas Lochbihler 2012-05-31 unify Card_Univ and Cardinality
2012-05-30 Andreas Lochbihler 2012-05-30 remove pretty syntax for FinFuns at the end and provide separate syntax theory
2012-05-30 Andreas Lochbihler 2012-05-30 eliminated remaining sub- and superscripts in FinFun syntax
2012-05-30 Andreas Lochbihler 2012-05-30 syntax for FinFun composition without subscripts tuned proofs
2012-05-30 Andreas Lochbihler 2012-05-30 FinFun pseudo-constructor syntax without superscripts
2012-05-30 Andreas Lochbihler 2012-05-30 replace FinFun application syntax with $
2012-05-30 Andreas Lochbihler 2012-05-30 removed subscripts from FinFun type syntax
2012-05-29 Andreas Lochbihler 2012-05-29 tuned proofs
2012-05-29 Andreas Lochbihler 2012-05-29 use bundle in FinFun
2012-05-29 Andreas Lochbihler 2012-05-29 unify Rep_finfun and finfun_apply
2012-05-29 Andreas Lochbihler 2012-05-29 move FinFuns from AFP to repository