| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 14:25:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 20:36:33 +0200 |
wenzelm |
support 'when' statement, which corresponds to 'presume';
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 10:54:53 +0100 |
wenzelm |
proper context and method setup;
|
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
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:07:47 +0100 |
wenzelm |
tuned signature -- rearranged modules;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 17:20:11 +0100 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 13:46:45 +0100 |
wenzelm |
eliminated legacy 'axioms';
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:15:02 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 13:29:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 11:42:43 +0200 |
wenzelm |
modernized functor names;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 15:07:35 +0200 |
wenzelm |
proper configuration option "show_proofs";
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 12:26:48 +0200 |
haftmann |
deglobalization
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 23:35:43 +0200 |
wenzelm |
mark schematic statements explicitly;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 15:50:41 +0100 |
wenzelm |
eliminated unnamed infixes;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:19:58 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 11:31:07 +0100 |
wenzelm |
fixed assumption proof;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|