src/HOL/Predicate.thy
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
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Fri, 06 Apr 2012 19:23:51 +0200 haftmann abandoned almost redundant *_foldr lemmas
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Fri, 24 Feb 2012 07:30:24 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Thu, 23 Feb 2012 20:33:35 +0100 haftmann moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
Sun, 19 Feb 2012 15:30:35 +0100 haftmann distributed lattice properties of predicates to places of instantiation
Thu, 12 Jan 2012 00:13:37 +0100 berghofe Added inf_Int_eq to pred_set_conv database as well
Tue, 10 Jan 2012 18:09:09 +0100 berghofe Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
Thu, 29 Dec 2011 15:14:44 +0100 haftmann conversions from sets to predicates and vice versa; extensionality on predicates
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Fri, 25 Nov 2011 13:14:58 +0100 wenzelm proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Tue, 23 Aug 2011 07:14:09 +0200 haftmann tuned specifications, syntax and proofs
Mon, 22 Aug 2011 22:00:36 +0200 haftmann tuned specifications and syntax
Sun, 21 Aug 2011 19:47:52 +0200 haftmann avoid pred/set mixture
Thu, 04 Aug 2011 20:11:39 +0200 haftmann more fine-granular instantiation
Wed, 03 Aug 2011 23:21:53 +0200 haftmann more specific instantiation
Fri, 29 Jul 2011 19:47:55 +0200 haftmann tuned proofs
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Tue, 21 Dec 2010 17:52:23 +0100 haftmann tuned type_lifting declarations
Mon, 20 Dec 2010 15:37:25 +0100 haftmann type_lifting for predicates
Wed, 08 Dec 2010 15:05:46 +0100 haftmann bot comes before top, inf before sup etc.
Wed, 08 Dec 2010 14:52:23 +0100 haftmann nice syntax for lattice INFI, SUPR;
Wed, 08 Dec 2010 13:34:50 +0100 haftmann primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
Mon, 29 Nov 2010 12:14:46 +0100 haftmann moved generic definitions about relations from Quotient.thy to Predicate;
Mon, 22 Nov 2010 17:48:35 +0100 haftmann adhere established Collect/mem convention more closely
Fri, 19 Nov 2010 14:35:58 +0100 haftmann eval simp rules for predicate type, simplify primitive proofs
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Mon, 23 Aug 2010 14:51:56 +0200 blanchet "no_atp" fact that leads to unsound Sledgehammer proofs
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Thu, 24 Jun 2010 21:01:13 +0200 blanchet yields ill-typed ATP/metis proofs -- raus!
Thu, 29 Apr 2010 15:00:40 +0200 haftmann code_reflect: specify module name directly after keyword
Wed, 28 Apr 2010 16:56:18 +0200 haftmann avoid code_datatype antiquotation
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Sun, 28 Mar 2010 12:49:14 -0700 huffman add/change some lemmas about lattices
Fri, 11 Dec 2009 14:43:56 +0100 haftmann moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
Sat, 05 Dec 2009 20:02:21 +0100 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices
Fri, 04 Dec 2009 18:19:30 +0100 haftmann tuned code setup
Thu, 19 Nov 2009 08:25:53 +0100 bulwahn adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
less more (0) -60 tip