| Wed, 29 Jun 2011 11:58:35 +0200 |
boehmes |
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
|
file |
diff |
annotate
|
| Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
clarify warning message to avoid confusing beginners
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 11:06:22 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:42:09 +0200 |
wenzelm |
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 17:37:26 +0200 |
wenzelm |
slightly more abstract data handling in Fast_Lin_Arith;
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 14:09:56 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| 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, 22 Mar 2010 11:45:09 +0100 |
boehmes |
removed warning_count (known causes for warnings have been resolved)
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 09:39:10 +0100 |
boehmes |
removed e-mail address from error message
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 16:44:12 +0100 |
wenzelm |
removed old CVS Ids;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 16:30:43 +0100 |
hoelzl |
Use same order of neq-elimination as in proof search.
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:49:44 +0100 |
wenzelm |
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 22:56:14 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
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
|
| Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 12:20:43 +0200 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 22:24:13 +0200 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
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
|
| Fri, 10 Jul 2009 07:59:27 +0200 |
haftmann |
dropped find_index_eq
|
file |
diff |
annotate
|