clarified signature;
more careful treatment of implicit context;

tuned messages;

proper context;

misc tuning and clarification, notably wrt. flow of context;

isabelle update -u control_cartouches;

more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
tuned signature;

added HOLogic.mk_obj_eq convenience and eliminated some clones;

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

PIDE reports of implicit variable scope;

tuned signature;

clarified check_open_spec / read_open_spec;
allow 'for' fixes in 'abbreviation', 'definition';

tuned proofs, to allow unfold_abs_def;

tuned;

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

within a proof body context, undeclared frees are like global constants;
tuned signature;

clarified signature;

eliminated "xname" and variants;

proper formatting via Pretty.string_of;
tuned;

clarified type Token.src: plain token list, with usual implicit value assignment;
clarified type Token.name_value, notably for head of Token.src;
clarified Attrib/Method check_src vs. parser;

moved remaining display.ML to more_thm.ML;

updated to infer_instantiate;

make SML/NJ more happy;

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

@{command_spec} is superseded by @{command_keyword};

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified signature;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

default abstypes and default abstract equations make technical (no_code) annotation superfluous

--HG--
extra : rebase_source : d54bb7382702f44984b3e0e4b39bf01c86d63963

abstract code equation may also be default

--HG--
extra : rebase_source : fca42b5b5bc30699c7fb8288302687df6f55905b

publish lifting_forget and lifting_udpate interface

note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional

more robust bundle_name: avoid assumptions about identifier, keywords etc.;

tuned signature;

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;

explicit type Keyword.keywords;
tuned signature;

tuned signature -- define some elementary operations earlier;

tuned signature -- moved type src to Token, without aliases;

tuned signature according to Scala version -- prefer explicit argument;

store explicitly quotient types with no_code => more precise registration of code equations

more appropriate name (Lifting.invariant -> eq_onp)

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

more antiquotations;

proper Args.syntax for slightly odd bundle trickery;
do not handle arbitrary exceptions;
more abstract type Args.src;

clarified Args.src: more abstract type, position refers to name only;
prefer self-contained Args.check_src;

tuned signature -- prefer Name_Space.get with its builtin error;

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

abstract type must be a type constructor; check it

update documentation of important public ML functions in Lifting

don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.

make SML/NJ happy

restoring Transfer/Lifting context

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure

stronger reflexivity prover

better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned

tuned command descriptions;

generate a parameterized correspondence relation

simplified code

generate correct correspondence relation name

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

quot_del attribute, it allows us to deregister quotient types

note Quotient theorem for typedefs in setup_lifting

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

infrastructure that makes possible to prove that a relation is reflexive

lifting package produces abs_eq_iff rules for total quotients

documentation of the Lifting package on the ML level & tuned

tuned; don't generate abs code if quotient_type is used

move MRSL to a separate file

setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq

--HG--
extra : rebase_source : d334e698d0b17a96fd23eb640133197a1cc23a6c

rename no_code to no_abs_code - more appropriate name

create thm names correctly

generate abs_induct rules for quotient types

--HG--
extra : rebase_source : 9656ecaf26f12a5d2b81ce9d2d260be2c75c910b

setup_lifting: no_code switch and supoport for quotient theorems

Lifting: generate more thms & note them & tuned

lifting_setup generates transfer rule for rep of typedefs

--HG--
extra : rebase_source : d0ceef760c5bb5d2f87dc38f6f2426ef0ce511f1

use context block to organize typedef lifting theorems

--HG--
extra : rebase_source : eb93bd18a5176c8cde5ba30ac6f536d2644e011c

tuned the setup of lifting; generate transfer rules for typedef and Quotient thms

detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr

support non-open typedefs; define cr_rel in terms of a rep function for typedefs

fix typos

--HG--
extra : transplant_source : x%EA%28%04%1F%BD%E9%8B%04%CA%00%FC%7F%EAaX%D1Z%B2m

fix typo in ML structure name

--HG--
extra : transplant_source : %10%0D%BDv%C1%10Z%9A%EF%17l%C8Q%D6%8B%B5%C0%F0%2B%FA

new package Lifting - initial commit