| Fri, 23 Feb 2018 14:32:59 +0100 |
wenzelm |
tuned signature -- eliminated clones;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:47 +0200 |
haftmann |
avoid Local_Theory.reset in application space
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 17:25:28 +0200 |
wenzelm |
clarified derived bindings (for PIDE reports);
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 12:49:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 14:35:48 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
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
|
file |
diff |
annotate
|
| Mon, 13 Apr 2015 15:27:34 +0200 |
kuncar |
go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
return also which code equation was used; tuned
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
export the result of lifting_def
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
improve handling of predicators in rsp_thm
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
lift_definition: return the result of lifting
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
lift_definition: interface also with tactic
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
generalize prove_schematic_quot_thm
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:38:59 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2015 08:29:08 +0100 |
haftmann |
abstract code equation may also be default
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 20:21:59 +0200 |
kuncar |
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 20:21:34 +0200 |
kuncar |
store explicitly quotient types with no_code => more precise registration of code equations
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 13:01:49 +0200 |
kuncar |
prevent beta-contraction in proving extra assumptions for abs_eq
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 22:19:37 +0200 |
kuncar |
fix the reflexivity prover
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:18 +0200 |
kuncar |
setup for Transfer and Lifting from BNF; tuned thm names
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
more appropriate name (Lifting.invariant -> eq_onp)
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 13:52:33 +0100 |
kuncar |
hide Lifting.invariant from a user completely
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 19:07:40 +0100 |
kuncar |
new rule for making rsp theorem more readable
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 15:02:54 +0100 |
kuncar |
the rules are not needed due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 15:02:19 +0100 |
kuncar |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 18:12:41 +0100 |
kuncar |
more robust registration of code equations
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 18:12:40 +0100 |
kuncar |
be consistent and produce always rep_eq with =
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:33 +0100 |
kuncar |
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:32 +0100 |
kuncar |
refactoring
|
file |
diff |
annotate
|
| Thu, 20 Feb 2014 16:56:32 +0100 |
kuncar |
the rule is not needed due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:47 +0100 |
kuncar |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 23:35:05 +0100 |
wenzelm |
more accurate context;
|
file |
diff |
annotate
|
| Wed, 08 Jan 2014 17:00:03 +0100 |
kuncar |
typo
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Mon, 14 Oct 2013 15:01:41 +0200 |
kuncar |
update documentation of important public ML functions in Lifting
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
allow to specify multiple parametricity transfer rules in lift_definition
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:17 +0200 |
kuncar |
restoring Transfer/Lifting context
|
file |
diff |
annotate
|
| Mon, 26 Aug 2013 16:13:20 +0200 |
wenzelm |
prefer Binding.name_of over Binding.print -- the latter leads to funny quotes and markup within the constructed term;
|
file |
diff |
annotate
|