| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some 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
|
| 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
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Mon, 23 May 2016 20:45:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 20:37:24 +0200 |
wenzelm |
within a proof body context, undeclared frees are like global constants;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:11:02 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2015 13:03:41 +0100 |
wenzelm |
proper formatting via Pretty.string_of;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
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
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
publish lifting_forget and lifting_udpate interface
|
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
|
| 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, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Fri, 06 Feb 2015 17:57:03 +0100 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file |
diff |
annotate
|
| Wed, 28 Jan 2015 08:29:08 +0100 |
haftmann |
abstract code equation may also be default
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 15:22:27 +0100 |
wenzelm |
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 14:04:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Wed, 05 Nov 2014 20:20:57 +0100 |
wenzelm |
explicit type Keyword.keywords;
|
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
|
| Tue, 12 Aug 2014 20:18:27 +0200 |
wenzelm |
tuned signature according to Scala version -- prefer explicit argument;
|
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, 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
|
| Sat, 22 Mar 2014 21:40:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 21:40:39 +0100 |
wenzelm |
proper Args.syntax for slightly odd bundle trickery;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 16:30:07 +0100 |
wenzelm |
clarified Args.src: more abstract type, position refers to name only;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 15:04:01 +0100 |
wenzelm |
tuned signature -- prefer Name_Space.get with its builtin error;
|
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, 15 Feb 2014 00:11:17 +0100 |
kuncar |
abstract type must be a type constructor; check it
|
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, 11 Oct 2013 18:36:51 +0200 |
kuncar |
don't allow parametricity theorem for typedefs in setup_lifting. The theorem is not used.
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 17:08:08 +0200 |
kuncar |
make SML/NJ happy
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:17 +0200 |
kuncar |
restoring Transfer/Lifting context
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 14:37:35 +0200 |
kuncar |
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 15:40:29 +0200 |
kuncar |
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
|
file |
diff |
annotate
|
| Wed, 15 May 2013 12:10:39 +0200 |
kuncar |
stronger reflexivity prover
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:14:23 +0100 |
kuncar |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
file |
diff |
annotate
|
| Thu, 29 Nov 2012 17:54:20 +0100 |
kuncar |
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 17:13:44 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:20:51 +0100 |
kuncar |
generate a parameterized correspondence relation
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Fri, 23 Nov 2012 15:53:24 +0100 |
kuncar |
simplified code
|
file |
diff |
annotate
|
| Fri, 23 Nov 2012 15:53:19 +0100 |
kuncar |
generate correct correspondence relation name
|
file |
diff |
annotate
|