src/HOL/Relation.thy
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-14 Andreas Lochbihler 2015-04-14 add lemmas
2015-02-11 Andreas Lochbihler 2015-02-11 add lemma
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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