| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Wed, 26 Jun 2013 21:48:23 +0200 |
wenzelm |
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 17:27:38 +0200 |
wenzelm |
obsolete -- tools should refer to proper Proof.context;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 17:13:21 +0100 |
wenzelm |
more formal cong_name;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:14:27 +0100 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
file |
diff |
annotate
|
| Sat, 17 Nov 2012 17:55:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 11 Aug 2012 22:17:46 +0200 |
wenzelm |
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2012 17:15:57 +0200 |
wenzelm |
outermost SELECT_GOAL potentially improves performance;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 19:26:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 23:55:03 +0100 |
wenzelm |
proper naming of simprocs according to actual target context;
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:52:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 19:29:54 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 21:51:46 +0100 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:15:47 +0100 |
wenzelm |
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 17:02:12 +0200 |
wenzelm |
added Name_Space.check/get convenience;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 16:30:00 +0200 |
wenzelm |
clarified check_simproc (with report) vs. the_simproc;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:53:09 +0200 |
wenzelm |
proper binding/report of defined simprocs;
|
file |
diff |
annotate
|