src/HOL/Predicate.thy
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
Thu, 12 Nov 2009 09:10:37 +0100 bulwahn removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
Wed, 11 Nov 2009 09:02:20 +0100 haftmann tuned
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn developing an executable the operator
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn generalizing singleton with a default value
Sat, 24 Oct 2009 16:54:32 +0200 bulwahn moved meta_fun_cong lemma into ML-file; tuned
Tue, 06 Oct 2009 18:44:06 +0200 haftmann inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
Wed, 30 Sep 2009 17:23:00 +0200 haftmann moved lemmas about sup on bool to Lattices.thy
Wed, 30 Sep 2009 17:04:21 +0200 haftmann tuned headings
Fri, 25 Sep 2009 09:50:31 +0200 haftmann merged
Wed, 23 Sep 2009 16:32:53 +0200 haftmann removed potentially dangerous rules from pred_set_conv
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added first prototype of the extended predicate compiler
Fri, 18 Sep 2009 09:07:48 +0200 haftmann be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
Tue, 15 Sep 2009 19:16:35 +0200 haftmann hide new constants
Tue, 15 Sep 2009 12:11:10 +0200 haftmann added emptiness check predicate and singleton projection
Fri, 14 Aug 2009 15:36:54 +0200 haftmann formally stylized
Mon, 27 Jul 2009 21:47:41 +0200 krauss "more standard" argument order of relation composition (op O)
Fri, 03 Jul 2009 16:51:06 +0200 haftmann avoid useless code equations
Thu, 21 May 2009 09:07:13 +0200 haftmann added Predicate.map in SML environment
Wed, 20 May 2009 22:24:07 +0200 haftmann added Predicate.map
Wed, 13 May 2009 18:41:36 +0200 haftmann dropped sort constraint on predicate equality
Tue, 12 May 2009 17:09:35 +0200 haftmann added dummy values keyword
Mon, 11 May 2009 19:54:24 +0200 haftmann avoid latex output problem
Mon, 11 May 2009 17:20:52 +0200 haftmann merged
Mon, 11 May 2009 09:18:42 +0200 bulwahn Added pred_code command
Wed, 22 Apr 2009 11:10:23 +0200 bulwahn added general preprocessing of equality in predicates for code generation
Wed, 22 Apr 2009 19:09:19 +0200 haftmann fixed compilation of predicate types in ML environment
Fri, 17 Apr 2009 15:14:06 +0200 haftmann static compilation of enumeration type
Wed, 11 Mar 2009 08:45:47 +0100 haftmann explicit code equations for some rarely used pred operations
Mon, 09 Mar 2009 09:34:39 +0100 haftmann dropped eq_pred
Sun, 08 Mar 2009 15:25:29 +0100 haftmann refined enumeration implementation
less more (0) -60 tip