src/HOL/ex/FinFunPred.thy
2012-06-01 Andreas Lochbihler 2012-06-01 simplify card_UNIV type class, tuned proofs
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 unify Rep_finfun and finfun_apply
2012-05-29 Andreas Lochbihler 2012-05-29 move FinFuns from AFP to repository