src/HOL/Library/FinFun.thy
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