| 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
|
| Wed, 11 Aug 2010 18:03:02 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:50:29 +0200 |
wenzelm |
simplified/unified command setup;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 16:35:00 +0100 |
haftmann |
avoid negative indices as argument ot drop
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sun, 29 Nov 2009 12:56:30 +1100 |
kleing |
Expand nested abbreviations before applying dummy patterns.
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 19:56:06 +0100 |
wenzelm |
observe usual naming conventions;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 16:44:18 +0100 |
krauss |
find_theorems: respect conceal flag
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:56:02 +0100 |
wenzelm |
less hermetic ML;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:02:53 +0100 |
wenzelm |
renamed Proof.flat_goal to Proof.simple_goal;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
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 16:41:22 +1100 |
kleing |
find_theorems: better handling of abbreviations (by Timothy Bourke)
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 22:02:11 +0200 |
wenzelm |
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 00:32:00 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
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
|
| Wed, 17 Jun 2009 17:07:26 +0200 |
wenzelm |
more detailed start_timing/end_timing;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 15:14:48 +0200 |
wenzelm |
minor tuning according to Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Wed, 06 May 2009 10:55:47 +1000 |
Timothy Bourke |
Prototype introiff option for find_theorems.
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 20:40:25 +0200 |
wenzelm |
superficial tuning;
|
file |
diff |
annotate
|