src/HOL/BNF_Comp.thy
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-06 traytel 2014-03-06 rationalized imports
2014-03-06 traytel 2014-03-06 move special BNFs used for composition only to BNF_Comp; use local copy of identity function that gets unfolded later for ID
2014-03-06 traytel 2014-03-06 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
2014-03-04 blanchet 2014-03-04 simplify sets in BNF composition
2014-03-03 blanchet 2014-03-03 adapted example
2014-03-03 blanchet 2014-03-03 life without 'metis'
2014-03-03 blanchet 2014-03-03 use same identity function for abs and rep (doesn't seem to confuse any proofs)
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-23 blanchet 2014-02-23 updated docs
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 tuned comments
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'