src/HOL/Tools/Lifting/lifting_setup.ML
2015-05-02 kuncar 2015-05-02 don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
2014-12-05 kuncar 2014-12-05 publish lifting_forget and lifting_udpate interface
2014-12-05 kuncar 2014-12-05 note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-02-06 haftmann 2015-02-06 default abstypes and default abstract equations make technical (no_code) annotation superfluous
2015-01-28 haftmann 2015-01-28 abstract code equation may also be default
2014-12-03 wenzelm 2014-12-03 more robust bundle_name: avoid assumptions about identifier, keywords etc.;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-07-24 kuncar 2014-07-24 store explicitly quotient types with no_code => more precise registration of code equations
2014-04-10 kuncar 2014-04-10 more appropriate name (Lifting.invariant -> eq_onp)
2014-04-10 kuncar 2014-04-10 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-10 wenzelm 2014-03-10 proper Args.syntax for slightly odd bundle trickery; do not handle arbitrary exceptions; more abstract type Args.src;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-10 wenzelm 2014-03-10 tuned signature -- prefer Name_Space.get with its builtin error;
2014-02-18 kuncar 2014-02-18 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
2014-02-15 kuncar 2014-02-15 abstract type must be a type constructor; check it
2013-10-14 kuncar 2013-10-14 update documentation of important public ML functions in Lifting
2013-10-11 kuncar 2013-10-11 don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.
2013-09-20 kuncar 2013-09-20 make SML/NJ happy
2013-09-16 kuncar 2013-09-16 restoring Transfer/Lifting context
2013-08-28 kuncar 2013-08-28 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
2013-08-07 kuncar 2013-08-07 expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-05-13 kuncar 2013-05-13 better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-03-08 kuncar 2013-03-08 lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
2012-11-29 kuncar 2012-11-29 parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
2012-11-26 wenzelm 2012-11-26 merged
2012-11-26 kuncar 2012-11-26 generate a parameterized correspondence relation
2012-11-26 wenzelm 2012-11-26 tuned command descriptions;
2012-11-23 kuncar 2012-11-23 simplified code
2012-11-23 kuncar 2012-11-23 generate correct correspondence relation name
2012-05-24 kuncar 2012-05-24 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
2012-05-21 kuncar 2012-05-21 quot_del attribute, it allows us to deregister quotient types
2012-05-18 kuncar 2012-05-18 note Quotient theorem for typedefs in setup_lifting
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-05-16 kuncar 2012-05-16 infrastructure that makes possible to prove that a relation is reflexive
2012-05-04 huffman 2012-05-04 lifting package produces abs_eq_iff rules for total quotients
2012-05-02 kuncar 2012-05-02 documentation of the Lifting package on the ML level & tuned
2012-04-26 kuncar 2012-04-26 tuned; don't generate abs code if quotient_type is used
2012-04-23 kuncar 2012-04-23 move MRSL to a separate file
2012-04-20 huffman 2012-04-20 setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
2012-04-19 kuncar 2012-04-19 rename no_code to no_abs_code - more appropriate name
2012-04-19 kuncar 2012-04-19 create thm names correctly
2012-04-19 huffman 2012-04-19 generate abs_induct rules for quotient types
2012-04-18 kuncar 2012-04-18 setup_lifting: no_code switch and supoport for quotient theorems
2012-04-18 kuncar 2012-04-18 Lifting: generate more thms & note them & tuned
2012-04-18 huffman 2012-04-18 lifting_setup generates transfer rule for rep of typedefs
2012-04-18 huffman 2012-04-18 use context block to organize typedef lifting theorems
2012-04-17 kuncar 2012-04-17 tuned the setup of lifting; generate transfer rules for typedef and Quotient thms