src/HOL/BNF_Comp.thy
Tue, 29 Jul 2014 23:39:35 +0200 blanchet header tuning
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Mon, 10 Mar 2014 13:23:16 +0100 traytel unfold intermediate definitions after sealing the bnf
Thu, 06 Mar 2014 14:15:09 +0100 traytel rationalized imports
Thu, 06 Mar 2014 14:14:54 +0100 traytel move special BNFs used for composition only to BNF_Comp;
Thu, 06 Mar 2014 12:17:26 +0100 traytel more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
Tue, 04 Mar 2014 18:57:17 +0100 blanchet simplify sets in BNF composition
Mon, 03 Mar 2014 12:48:20 +0100 blanchet adapted example
Mon, 03 Mar 2014 12:48:20 +0100 blanchet life without 'metis'
Mon, 03 Mar 2014 12:48:20 +0100 blanchet use same identity function for abs and rep (doesn't seem to confuse any proofs)
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'typedef' optional, depending on size of original type
Mon, 03 Mar 2014 12:48:19 +0100 blanchet optimize cardinal bounds involving natLeq (omega)
Fri, 28 Feb 2014 17:54:52 +0100 traytel load Metis a little later
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Sun, 23 Feb 2014 22:51:11 +0100 blanchet updated docs
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuning
Mon, 20 Jan 2014 18:24:56 +0100 blanchet made BNF compile after move to HOL
Mon, 20 Jan 2014 18:24:56 +0100 blanchet tuned comments
Mon, 20 Jan 2014 18:24:56 +0100 blanchet moved BNF files to 'HOL'
less more (0) tip