src/HOL/Quotient.thy
5 weeks ago wenzelm 2019-03-14 more specific keyword kinds;
3 months ago wenzelm 2019-01-06 isabelle update -u path_cartouches;
9 months ago paulson 2018-07-11 de-applying (mostly Quotient)
9 months ago paulson 2018-07-11 de-applying
15 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
16 months ago wenzelm 2017-11-26 more symbols;
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-22 wenzelm 2014-11-22 named_theorems: multiple args;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems; modernized setup;
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2013-12-26 haftmann 2013-12-26 prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm
2013-11-21 blanchet 2013-11-21 rationalize imports
2013-08-13 kuncar 2013-08-13 introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
2013-02-14 haftmann 2013-02-14 abandoned theory Plain
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-20 huffman 2012-04-20 move definition of set_rel into Library/Quotient_Set.thy
2012-04-19 huffman 2012-04-19 tuned lemmas (v)image_id; removed duplicate of vimage_id
2012-04-18 huffman 2012-04-18 move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients
2012-04-15 haftmann 2012-04-15 centralized enriched_type declaration, thanks to in-situ available Isar commands
2012-04-12 bulwahn 2012-04-12 merged
2012-04-04 griff 2012-04-04 manual merge
2012-04-03 griff 2012-04-03 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-04 kuncar 2012-04-04 connect the Quotient package to the Lifting package
2012-04-04 kuncar 2012-04-04 support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-23 kuncar 2012-03-23 hide invariant constant
2012-03-23 kuncar 2012-03-23 generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
2012-03-23 kuncar 2012-03-23 store the relational theorem for every relator
2012-03-23 kuncar 2012-03-23 respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-02-14 wenzelm 2012-02-14 simplified use of tacticals;
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-12-09 kuncar 2011-12-09 Quotient_Info stores only relation maps
2011-12-07 Christian Urban 2011-12-07 added a specific tactic and method that deal with partial equivalence relations
2011-11-29 wenzelm 2011-11-29 more conventional file name;
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-26 haftmann 2011-08-26 avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
2011-08-23 Cezary Kaliszyk 2011-08-23 Quotient Package: some infrastructure for lifting inside sets
2011-08-16 haftmann 2011-08-16 avoid Collect_def in proof
2011-08-16 Cezary Kaliszyk 2011-08-16 Quotient Package: make quotient_type work with separate set type
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-04-14 blanchet 2011-04-14 use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-07 wenzelm 2011-01-07 more standard package setup;
2010-11-29 haftmann 2010-11-29 reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text
2010-11-29 haftmann 2010-11-29 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; moved generic definitions about relations from Quotient.thy to Predicate; consistent use of R rather than E for relations; more natural deduction rules
2010-11-19 haftmann 2010-11-19 generalized type
2010-11-18 haftmann 2010-11-18 map_fun combinator in theory Fun
2010-11-09 haftmann 2010-11-09 type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
2010-10-19 Cezary Kaliszyk 2010-10-19 Quotient package: partial equivalence introduction
2010-10-05 blanchet 2010-10-05 remove needless Metis facts
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-09-24 Cezary Kaliszyk 2010-09-24 quotient package: respectfulness and preservation of identity.
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