| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 17:56:18 +0100 |
berghofe |
Specific theorems in a named list of theorems can now be referred to
|
file |
diff |
annotate
|
| Tue, 28 Sep 2004 13:54:49 +0200 |
ballarin |
Bug fixes.
|
file |
diff |
annotate
|
| Mon, 27 Sep 2004 10:27:34 +0200 |
ballarin |
Modified locales: improved implementation of "includes".
|
file |
diff |
annotate
|
| Thu, 12 Aug 2004 10:01:09 +0200 |
ballarin |
Disallowed "includes" in locale declarations.
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 14:48:59 +0200 |
ballarin |
Typo.
|
file |
diff |
annotate
|
| Mon, 02 Aug 2004 10:16:58 +0200 |
ballarin |
Some comments added.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:19:47 +0200 |
wenzelm |
TypeInfer.paramify_dummies, TypeInfer.param;
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:08:57 +0200 |
wenzelm |
improved Term.invent_names;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 13:28:46 +0200 |
wenzelm |
renamed have_thms to note_thms;
|
file |
diff |
annotate
|
| Wed, 07 Apr 2004 20:42:13 +0200 |
ballarin |
Locale instantiation: label parameter optional, new attribute paramter.
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 14:08:30 +0200 |
ballarin |
Experimental command for instantiation of locales in proof contexts:
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 12:18:19 +0100 |
ballarin |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 11 Dec 2003 14:10:27 +0100 |
ballarin |
Change to prune_prems in Pure/Isar/locale.ML.
|
file |
diff |
annotate
|
| Thu, 06 Nov 2003 14:18:05 +0100 |
ballarin |
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
|
file |
diff |
annotate
|
| Tue, 30 Sep 2003 17:05:50 +0200 |
ballarin |
Removed garbage accidentally left behind in file.
|
file |
diff |
annotate
|
| Tue, 30 Sep 2003 15:13:02 +0200 |
ballarin |
Improvements to Isar/Locales: premises generated by "includes" elements
|
file |
diff |
annotate
|
| Mon, 07 Oct 2002 19:01:51 +0200 |
nipkow |
take/drop -> splitAt
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:19:52 +0200 |
wenzelm |
predefined locales "var" and "struct" (useful for sharing parameters);
|
file |
diff |
annotate
|
| Fri, 02 Aug 2002 11:12:34 +0200 |
wenzelm |
declare projected "axioms" as "elim?";
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 22:14:42 +0200 |
wenzelm |
removed unused locale_facts(_i);
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 00:12:50 +0200 |
wenzelm |
tuned view;
|
file |
diff |
annotate
|
| Fri, 19 Jul 2002 18:44:07 +0200 |
wenzelm |
support locale ``views'' (for cumulative predicates);
|
file |
diff |
annotate
|
| Thu, 18 Jul 2002 12:10:24 +0200 |
wenzelm |
define cumulative predicate view;
|
file |
diff |
annotate
|
| Tue, 16 Jul 2002 18:41:00 +0200 |
wenzelm |
proper predicate definitions of locale body;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 14:51:18 +0200 |
wenzelm |
tuned add_thmss;
|
file |
diff |
annotate
|
| Mon, 08 Jul 2002 11:34:43 +0200 |
wenzelm |
clarified text content of locale body;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2002 16:48:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Jun 2002 17:22:10 +0200 |
wenzelm |
BUG FIX in inst_thm: use current context instead of that of thm!!!
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 21:46:03 +0100 |
wenzelm |
added smart_have_thmss (global storage);
|
file |
diff |
annotate
|
| Wed, 30 Jan 2002 13:59:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Jan 2002 16:58:26 +0100 |
wenzelm |
reorganized code for predicate text;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2002 21:18:36 +0100 |
wenzelm |
added locale_facts(_i) interface (useful for simple ML proof tools);
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:05:40 +0100 |
wenzelm |
ObjectLogic.atomize_term replaces ObjectLogic.atomize_cterm;
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 00:11:30 +0100 |
wenzelm |
print_locale: allow full body specification;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 22:17:08 +0100 |
wenzelm |
produce predicate text;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:40:02 +0100 |
wenzelm |
unify_frozen: proper use of maxidx';
|
file |
diff |
annotate
|
| Fri, 11 Jan 2002 00:29:54 +0100 |
wenzelm |
have_thmss vs. have_thmss_i;
|
file |
diff |
annotate
|
| Thu, 10 Jan 2002 21:04:15 +0100 |
wenzelm |
removed add_thmss;
|
file |
diff |
annotate
|
| Thu, 10 Jan 2002 16:04:42 +0100 |
wenzelm |
add_thmss_hybrid;
|
file |
diff |
annotate
|
| Wed, 09 Jan 2002 13:51:26 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Fri, 21 Dec 2001 15:18:07 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 21 Dec 2001 00:40:16 +0100 |
wenzelm |
fixed inst_thm: proper domain of env;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 00:26:04 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2001 02:22:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 18 Dec 2001 02:19:31 +0100 |
wenzelm |
simultaneous type-inference of complete context/statement specifications;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 22:32:52 +0100 |
wenzelm |
removed debug stuff;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 22:28:52 +0100 |
wenzelm |
proper treatment of internal parameters;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 11:55:34 +0100 |
wenzelm |
beginning support for type instantiation;
|
file |
diff |
annotate
|
| Thu, 29 Nov 2001 01:50:19 +0100 |
wenzelm |
qualify_elem: do not qualify empty names ("");
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:42:04 +0100 |
wenzelm |
qualify imported facts;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2001 16:59:32 +0100 |
wenzelm |
clarified locale operations (rename, merge);
|
file |
diff |
annotate
|
| Fri, 23 Nov 2001 19:20:06 +0100 |
wenzelm |
improved ordering of evaluated elements;
|
file |
diff |
annotate
|
| Thu, 22 Nov 2001 23:45:57 +0100 |
wenzelm |
beginnings of actual locale expressions;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 20:20:18 +0100 |
wenzelm |
locale expressions;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:34:09 +0100 |
wenzelm |
added add_thmss;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:16:07 +0100 |
wenzelm |
proper close_locale;
|
file |
diff |
annotate
|