src/HOL/Predicate.thy
2010-04-29 haftmann code_reflect: specify module name directly after keyword
2010-04-28 haftmann avoid code_datatype antiquotation
2010-04-16 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-28 huffman add/change some lemmas about lattices
2009-12-11 haftmann moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
2009-12-05 haftmann tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann tuned code setup
2009-11-19 bulwahn adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
2009-11-12 bulwahn removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
2009-11-11 haftmann tuned
2009-10-24 bulwahn developing an executable the operator
2009-10-24 bulwahn generalizing singleton with a default value
2009-10-24 bulwahn moved meta_fun_cong lemma into ML-file; tuned
2009-10-06 haftmann inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-09-30 haftmann moved lemmas about sup on bool to Lattices.thy
2009-09-30 haftmann tuned headings
2009-09-25 haftmann merged
2009-09-23 haftmann removed potentially dangerous rules from pred_set_conv
2009-09-23 bulwahn added first prototype of the extended predicate compiler
2009-09-18 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
2009-09-15 haftmann hide new constants
2009-09-15 haftmann added emptiness check predicate and singleton projection
2009-08-14 haftmann formally stylized
2009-07-27 krauss "more standard" argument order of relation composition (op O)
2009-07-03 haftmann avoid useless code equations
2009-05-21 haftmann added Predicate.map in SML environment
2009-05-20 haftmann added Predicate.map
2009-05-13 haftmann dropped sort constraint on predicate equality
2009-05-12 haftmann added dummy values keyword
2009-05-11 haftmann avoid latex output problem
less more (0) -30 tip