2014-09-06 haftmann 2014-09-06 added various facts
2014-05-29 nipkow 2014-05-29 typo
2014-04-29 wenzelm 2014-04-29 prefer plain ASCII / latex over not-so-universal Unicode;
2014-04-26 haftmann 2014-04-26 more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
2014-03-13 blanchet 2014-03-13 killed a few 'metis' calls
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-21 traytel 2014-01-21 removed theory dependency of BNF_LFP on Datatype
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2013-11-29 traytel 2013-11-29 set_comprehension_pointfree simproc causes to many surprises if enabled by default
2013-11-21 blanchet 2013-11-21 rationalize imports
2013-11-12 hoelzl 2013-11-12 countability of the image of a reflexive transitive closure
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-17 nipkow 2013-09-17 added lemmas and made concerse executable
2013-07-28 traytel 2013-07-28 more converse(p) theorems; tuned proofs;
2013-07-25 traytel 2013-07-25 two useful relation theorems
2013-06-19 nipkow 2013-06-19 added lemma
2012-12-07 nipkow 2012-12-07 corrected nonsensical associativity of `` and dvd
2012-07-31 kuncar 2012-07-31 more relation operations expressed by Finite_Set.fold
2012-07-12 bulwahn 2012-07-12 a first guess to avoid the Codegenerator_Test to loop infinitely
2012-05-16 kuncar 2012-05-16 generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-04-12 bulwahn 2012-04-12 merged
2012-04-03 griff 2012-04-03 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-05 huffman 2012-04-05 define reflp directly, in the manner of symp and transp
2012-03-22 haftmann 2012-03-22 fixed typo
2012-03-17 haftmann 2012-03-17 spelt out missing colemmas
2012-03-17 haftmann 2012-03-17 generalized INF_INT_eq, SUP_UN_eq
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-03-12 noschinl 2012-03-12 tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-03-07 haftmann 2012-03-07 tuned syntax; more candidates
2012-03-02 haftmann 2012-03-02 more fundamental pred-to-set conversions for range and domain by means of inductive_set
2012-03-01 haftmann 2012-03-01 more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
2012-02-26 haftmann 2012-02-26 restored accidental omission
2012-02-26 haftmann 2012-02-26 tuned structure
2012-02-26 haftmann 2012-02-26 tuned structure; dropped already existing syntax declarations
2012-02-26 haftmann 2012-02-26 tuned syntax declarations; tuned structure
2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-24 haftmann 2012-02-24 explicit remove of lattice notation
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-01-30 nipkow 2012-01-30 added "'a rel"
2012-01-01 haftmann 2012-01-01 cleanup of code declarations
2011-12-24 haftmann 2011-12-24 dropped obsolete code equation for Id
2011-10-13 haftmann 2011-10-13 moved acyclic predicate up in hierarchy
2011-10-13 haftmann 2011-10-13 modernized definitions
2011-09-20 haftmann 2011-09-20 tuned specification and lemma distribution among theories; tuned proofs
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2010-12-07 bulwahn 2010-12-07 adding a definition for refl_on which is friendly for quickcheck and nitpick
2010-12-03 bulwahn 2010-12-03 adding a nice definition of Id_on for quickcheck and nitpick
2010-05-09 krauss 2010-05-09 added lemmas rel_comp_UNION_distrib(2)
2010-05-07 krauss 2010-05-07 removed semicolons
2010-05-07 krauss 2010-05-07 rule subrelI (for nice Isar proofs of relation inequalities)
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2009-10-26 krauss 2009-10-26 lemma converse_inv_image