| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Mon, 03 May 2010 16:26:47 +0200 |
wenzelm |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 21:38:38 +0100 |
wenzelm |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 23:05:47 +0100 |
wenzelm |
use simplified Syntax.escape;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 16:11:45 +0100 |
wenzelm |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:56:33 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:10:35 +0200 |
wenzelm |
space_implode;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 16:15:22 +0200 |
wenzelm |
sort_strings (cf. Pure/library.ML);
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 21:04:03 +0200 |
wenzelm |
modernized messages -- eliminated ctyp/cterm operations;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 22:31:27 +0200 |
wenzelm |
ML_Context.the_local_context;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:02:34 +0200 |
wenzelm |
explicit OldGoals;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:49 +0100 |
haftmann |
stripped dead code
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 23:30:58 +0100 |
wenzelm |
minimal adaptions for abstract binding type;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 18:27:43 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|