Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Thu, 03 Jan 2019 22:19:19 +0100 |
wenzelm |
isabelle update_inner_syntax_cartouches;
|
file |
diff |
annotate
|
Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
Wed, 22 Jun 2016 10:40:53 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
Wed, 16 Dec 2015 16:31:36 +0100 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|
Mon, 14 Dec 2015 11:20:31 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
Sun, 30 Aug 2015 22:07:55 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
Thu, 25 Jun 2015 16:14:00 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 25 Jun 2015 15:56:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 17:14:05 +0200 |
wenzelm |
implicit rule for method "cases";
|
file |
diff |
annotate
|
Sat, 30 May 2015 20:21:53 +0200 |
wenzelm |
tuned -- more direct Thm.renamed_prop;
|
file |
diff |
annotate
|
Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 20:14:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 19:58:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
Mon, 06 Apr 2015 12:37:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 29 Mar 2015 20:40:49 +0200 |
wenzelm |
tuned;
|
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
|