src/HOL/Predicate.thy
2011-11-25 wenzelm 2011-11-25 proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-08-23 haftmann 2011-08-23 tuned specifications, syntax and proofs
2011-08-22 haftmann 2011-08-22 tuned specifications and syntax
2011-08-21 haftmann 2011-08-21 avoid pred/set mixture
2011-08-04 haftmann 2011-08-04 more fine-granular instantiation
2011-08-03 haftmann 2011-08-03 more specific instantiation
2011-07-29 haftmann 2011-07-29 tuned proofs
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations
2010-12-20 haftmann 2010-12-20 type_lifting for predicates
2010-12-08 haftmann 2010-12-08 bot comes before top, inf before sup etc.
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-29 haftmann 2010-11-29 moved generic definitions about relations from Quotient.thy to Predicate; more natural deduction rules
2010-11-22 haftmann 2010-11-22 adhere established Collect/mem convention more closely
2010-11-19 haftmann 2010-11-19 eval simp rules for predicate type, simplify primitive proofs
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-23 blanchet 2010-08-23 "no_atp" fact that leads to unsound Sledgehammer proofs
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-24 blanchet 2010-06-24 yields ill-typed ATP/metis proofs -- raus!
2010-04-29 haftmann 2010-04-29 code_reflect: specify module name directly after keyword
2010-04-28 haftmann 2010-04-28 avoid code_datatype antiquotation
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-28 huffman 2010-03-28 add/change some lemmas about lattices
2009-12-11 haftmann 2009-12-11 moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann 2009-12-04 tuned code setup
2009-11-19 bulwahn 2009-11-19 adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
2009-11-12 bulwahn 2009-11-12 removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
2009-11-11 haftmann 2009-11-11 tuned
2009-10-24 bulwahn 2009-10-24 developing an executable the operator
2009-10-24 bulwahn 2009-10-24 generalizing singleton with a default value
2009-10-24 bulwahn 2009-10-24 moved meta_fun_cong lemma into ML-file; tuned
2009-10-06 haftmann 2009-10-06 inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-09-30 haftmann 2009-09-30 moved lemmas about sup on bool to Lattices.thy
2009-09-30 haftmann 2009-09-30 tuned headings
2009-09-25 haftmann 2009-09-25 merged
2009-09-23 haftmann 2009-09-23 removed potentially dangerous rules from pred_set_conv
2009-09-23 bulwahn 2009-09-23 added first prototype of the extended predicate compiler
2009-09-18 haftmann 2009-09-18 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
2009-09-15 haftmann 2009-09-15 hide new constants
2009-09-15 haftmann 2009-09-15 added emptiness check predicate and singleton projection
2009-08-14 haftmann 2009-08-14 formally stylized
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-07-03 haftmann 2009-07-03 avoid useless code equations
2009-05-21 haftmann 2009-05-21 added Predicate.map in SML environment
2009-05-20 haftmann 2009-05-20 added Predicate.map
2009-05-13 haftmann 2009-05-13 dropped sort constraint on predicate equality
2009-05-12 haftmann 2009-05-12 added dummy values keyword
2009-05-11 haftmann 2009-05-11 avoid latex output problem
2009-05-11 haftmann 2009-05-11 merged
2009-05-11 bulwahn 2009-05-11 Added pred_code command
2009-04-22 bulwahn 2009-04-22 added general preprocessing of equality in predicates for code generation
2009-04-22 haftmann 2009-04-22 fixed compilation of predicate types in ML environment
2009-04-17 haftmann 2009-04-17 static compilation of enumeration type
2009-03-11 haftmann 2009-03-11 explicit code equations for some rarely used pred operations