| Mon, 20 Jul 2009 21:20:09 +0200 |
wenzelm |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:33:11 +0100 |
wenzelm |
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:11 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 20:43:59 +0200 |
wenzelm |
TextIO.inputLine: non-critical (assume exclusive ownership);
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:23 +0200 |
wenzelm |
tuned goal conversion interfaces;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 22:27:30 +0200 |
wenzelm |
CONVERSION: handle TYPE | TERM | CTERM | THM;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
added CONVERSION tactical;
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 13:16:44 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:52 +0200 |
wenzelm |
added CSUBGOAL;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 01:25:24 +0200 |
wenzelm |
TextIO.inputLine: use present SML B library version;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:00 +0200 |
wenzelm |
renamed Term.variant_abs to Syntax.variant_abs;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:00 +0200 |
wenzelm |
tuned Seq/Envir/Unify interfaces;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:29 +0200 |
wenzelm |
avoid low-level Term.str_of_term;
|
file |
diff |
annotate
|
| Mon, 24 Apr 2006 16:36:07 +0200 |
haftmann |
cleaned up some diagnostic mathom
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 04:02:53 +0100 |
mengj |
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
|
file |
diff |
annotate
|
| Tue, 28 Feb 2006 11:07:54 +0100 |
paulson |
splitting up METAHYPS into smaller functions
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:49 +0200 |
wenzelm |
moved SELECT_GOAL to goal.ML;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:28 +0200 |
wenzelm |
Seq.maps;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 09:35:30 +0200 |
wenzelm |
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 09:11:32 +0200 |
wenzelm |
header;
|
file |
diff |
annotate
|