#
ca7bf8cb |
|
06-Aug-2019 |
wenzelm <none@none> |
clarified signature; more careful treatment of implicit context;
|
#
5e953f59 |
|
04-Jun-2019 |
wenzelm <none@none> |
tuned messages;
|
#
44401f83 |
|
04-Jun-2019 |
wenzelm <none@none> |
proper context;
|
#
0c041064 |
|
04-Jun-2019 |
wenzelm <none@none> |
misc tuning and clarification, notably wrt. flow of context;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
26e81017 |
|
27-Nov-2018 |
wenzelm <none@none> |
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;
|
#
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
#
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations --HG-- extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
#
a41e5df2 |
|
05-Jul-2016 |
wenzelm <none@none> |
PIDE reports of implicit variable scope;
|
#
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
#
cfdb609c |
|
29-May-2016 |
wenzelm <none@none> |
clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';
|
#
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
#
e6c4017e |
|
23-May-2016 |
wenzelm <none@none> |
tuned;
|
#
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
|
#
7455d7eb |
|
24-Apr-2016 |
wenzelm <none@none> |
within a proof body context, undeclared frees are like global constants; tuned signature;
|
#
ef845594 |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified signature;
|
#
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
#
072c0a61 |
|
20-Dec-2015 |
wenzelm <none@none> |
proper formatting via Pretty.string_of; tuned;
|
#
6eb38925 |
|
09-Dec-2015 |
wenzelm <none@none> |
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;
|
#
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
#
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
#
b74c761c |
|
03-May-2015 |
wenzelm <none@none> |
make SML/NJ more happy;
|
#
cd379f20 |
|
02-May-2015 |
kuncar <none@none> |
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
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
36b57329 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
d1684c4b |
|
06-Feb-2015 |
haftmann <none@none> |
default abstypes and default abstract equations make technical (no_code) annotation superfluous --HG-- extra : rebase_source : d54bb7382702f44984b3e0e4b39bf01c86d63963
|
#
81c350ec |
|
28-Jan-2015 |
haftmann <none@none> |
abstract code equation may also be default --HG-- extra : rebase_source : fca42b5b5bc30699c7fb8288302687df6f55905b
|
#
59bd4466 |
|
05-Dec-2014 |
kuncar <none@none> |
publish lifting_forget and lifting_udpate interface
|
#
417461b4 |
|
05-Dec-2014 |
kuncar <none@none> |
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
|
#
10bb035d |
|
03-Dec-2014 |
wenzelm <none@none> |
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
|
#
91c3d5c1 |
|
03-Dec-2014 |
wenzelm <none@none> |
tuned signature;
|
#
c12ca051 |
|
07-Nov-2014 |
wenzelm <none@none> |
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;
|
#
df4ccf3c |
|
05-Nov-2014 |
wenzelm <none@none> |
explicit type Keyword.keywords; tuned signature;
|
#
97ed7d8c |
|
21-Aug-2014 |
wenzelm <none@none> |
tuned signature -- define some elementary operations earlier;
|
#
d65030e5 |
|
19-Aug-2014 |
wenzelm <none@none> |
tuned signature -- moved type src to Token, without aliases;
|
#
0da05f9f |
|
12-Aug-2014 |
wenzelm <none@none> |
tuned signature according to Scala version -- prefer explicit argument;
|
#
0d029175 |
|
24-Jul-2014 |
kuncar <none@none> |
store explicitly quotient types with no_code => more precise registration of code equations
|
#
128e121b |
|
10-Apr-2014 |
kuncar <none@none> |
more appropriate name (Lifting.invariant -> eq_onp)
|
#
845456ae |
|
10-Apr-2014 |
kuncar <none@none> |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
#
9c548546 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
9d0c860b |
|
10-Mar-2014 |
wenzelm <none@none> |
proper Args.syntax for slightly odd bundle trickery; do not handle arbitrary exceptions; more abstract type Args.src;
|
#
0673c065 |
|
10-Mar-2014 |
wenzelm <none@none> |
clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
|
#
4bde3665 |
|
10-Mar-2014 |
wenzelm <none@none> |
tuned signature -- prefer Name_Space.get with its builtin error;
|
#
93867854 |
|
18-Feb-2014 |
kuncar <none@none> |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
#
15062e4c |
|
14-Feb-2014 |
kuncar <none@none> |
abstract type must be a type constructor; check it
|
#
63a445a7 |
|
14-Oct-2013 |
kuncar <none@none> |
update documentation of important public ML functions in Lifting
|
#
ce138e50 |
|
11-Oct-2013 |
kuncar <none@none> |
don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.
|
#
89364b2e |
|
20-Sep-2013 |
kuncar <none@none> |
make SML/NJ happy
|
#
308ade1d |
|
16-Sep-2013 |
kuncar <none@none> |
restoring Transfer/Lifting context
|
#
9e756f50 |
|
28-Aug-2013 |
kuncar <none@none> |
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
|
#
4378c6f4 |
|
07-Aug-2013 |
kuncar <none@none> |
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
|
#
01e7a4f2 |
|
14-May-2013 |
kuncar <none@none> |
stronger reflexivity prover
|
#
8c36fedb |
|
13-May-2013 |
kuncar <none@none> |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
#
f2065d73 |
|
08-Mar-2013 |
kuncar <none@none> |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
#
61291247 |
|
29-Nov-2012 |
kuncar <none@none> |
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
|
#
55014c61 |
|
26-Nov-2012 |
wenzelm <none@none> |
tuned command descriptions;
|
#
d5325b13 |
|
26-Nov-2012 |
kuncar <none@none> |
generate a parameterized correspondence relation
|
#
cb9f3170 |
|
23-Nov-2012 |
kuncar <none@none> |
simplified code
|
#
37821d6c |
|
23-Nov-2012 |
kuncar <none@none> |
generate correct correspondence relation name
|
#
dd23141d |
|
24-May-2012 |
kuncar <none@none> |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
#
eaf277a6 |
|
21-May-2012 |
kuncar <none@none> |
quot_del attribute, it allows us to deregister quotient types
|
#
1681db1d |
|
18-May-2012 |
kuncar <none@none> |
note Quotient theorem for typedefs in setup_lifting
|
#
7bae30d6 |
|
16-May-2012 |
kuncar <none@none> |
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
|
#
7e12d58a |
|
16-May-2012 |
kuncar <none@none> |
infrastructure that makes possible to prove that a relation is reflexive
|
#
4ede7bb5 |
|
04-May-2012 |
huffman <none@none> |
lifting package produces abs_eq_iff rules for total quotients
|
#
cc0ee287 |
|
02-May-2012 |
kuncar <none@none> |
documentation of the Lifting package on the ML level & tuned
|
#
16b75b0d |
|
26-Apr-2012 |
kuncar <none@none> |
tuned; don't generate abs code if quotient_type is used
|
#
a7ace5a5 |
|
23-Apr-2012 |
kuncar <none@none> |
move MRSL to a separate file
|
#
d12ecb3c |
|
20-Apr-2012 |
huffman <none@none> |
setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq --HG-- extra : rebase_source : d334e698d0b17a96fd23eb640133197a1cc23a6c
|
#
59dc94e2 |
|
19-Apr-2012 |
kuncar <none@none> |
rename no_code to no_abs_code - more appropriate name
|
#
0b02427e |
|
18-Apr-2012 |
kuncar <none@none> |
create thm names correctly
|
#
4a7f2f4a |
|
19-Apr-2012 |
huffman <none@none> |
generate abs_induct rules for quotient types --HG-- extra : rebase_source : 9656ecaf26f12a5d2b81ce9d2d260be2c75c910b
|
#
c3a03aa2 |
|
18-Apr-2012 |
kuncar <none@none> |
setup_lifting: no_code switch and supoport for quotient theorems
|
#
3e3d1772 |
|
18-Apr-2012 |
kuncar <none@none> |
Lifting: generate more thms & note them & tuned
|
#
f8111acb |
|
17-Apr-2012 |
huffman <none@none> |
lifting_setup generates transfer rule for rep of typedefs --HG-- extra : rebase_source : d0ceef760c5bb5d2f87dc38f6f2426ef0ce511f1
|
#
6b43d349 |
|
18-Apr-2012 |
huffman <none@none> |
use context block to organize typedef lifting theorems --HG-- extra : rebase_source : eb93bd18a5176c8cde5ba30ac6f536d2644e011c
|
#
b07286d9 |
|
17-Apr-2012 |
kuncar <none@none> |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
#
24024848 |
|
05-Apr-2012 |
kuncar <none@none> |
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
|
#
fe6190cb |
|
04-Apr-2012 |
kuncar <none@none> |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
#
d087b2e1 |
|
04-Apr-2012 |
huffman <none@none> |
fix typos --HG-- extra : transplant_source : x%EA%28%04%1F%BD%E9%8B%04%CA%00%FC%7F%EAaX%D1Z%B2m
|
#
fa8da735 |
|
04-Apr-2012 |
huffman <none@none> |
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
|
#
a2076df5 |
|
03-Apr-2012 |
kuncar <none@none> |
new package Lifting - initial commit
|