src/HOL/Predicate.thy
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 01 May 2015 17:52:24 +0200 wenzelm tuned spelling;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Sun, 04 May 2014 18:14:58 +0200 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Fri, 14 Feb 2014 07:53:46 +0100 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
Wed, 12 Feb 2014 08:35:57 +0100 blanchet adapted theories to 'xxx_case' to 'case_xxx'
Fri, 27 Sep 2013 08:59:22 +0200 Andreas Lochbihler prefer Code.abort over code_abort
less more (0) -100 -15 tip