| 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
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| 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
|
| Tue, 06 Jul 2004 20:32:20 +0200 |
schirmer |
print_tac now outputs goals through trace-channel
|
file |
diff |
annotate
|
| Fri, 25 Jun 2004 14:30:55 +0200 |
skalberg |
Merging the meta-simplifier with the Provers-simplifier. Next step:
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:12:44 +0200 |
berghofe |
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
|
file |
diff |
annotate
|
| Thu, 17 Oct 2002 10:52:59 +0200 |
paulson |
fixing the cut_tac method to work when there are no instantiations and the
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:27:54 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2002 19:15:51 +0100 |
wenzelm |
generic DETERM;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2001 23:52:45 +0100 |
wenzelm |
goals_limit moved to display.ML;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 23:28:01 +0200 |
wenzelm |
added RANGE (from Isar/proof.ML);
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:01:52 +0200 |
wenzelm |
Display.print_goals;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:12:15 +0200 |
berghofe |
Tidied function SELECT_GOAL.
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:41:56 +0100 |
wenzelm |
CHANGED_PROP;
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:18:31 +0100 |
wenzelm |
Thm: dest_comb, dest_abs, capply, cabs no longer global;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2000 18:46:53 +0100 |
wenzelm |
ALLGOALS_RANGE superceded by Seq.INTERVAL;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 17:50:28 +0100 |
wenzelm |
export ALLGOALS_RANGE;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2000 13:18:43 +0100 |
wenzelm |
added REPEAT_ALL_NEW;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 11:23:41 +0100 |
oheimb |
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 10:19:18 +0200 |
paulson |
fixed CHANGED_GOAL, which is used by stac
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:49:31 +0100 |
paulson |
Added a "message" argument to print_tac
|
file |
diff |
annotate
|
| Mon, 30 Nov 1998 10:45:39 +0100 |
paulson |
tactical CHANGED now uses alpha-eta conversion, not alpha conversion
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 13:59:06 +0100 |
wenzelm |
tuned space;
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 13:57:44 +0100 |
wenzelm |
replaced prs by writeln;
|
file |
diff |
annotate
|
| Tue, 17 Nov 1998 14:07:25 +0100 |
wenzelm |
Drule.rev_triv_goal;
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 17:44:50 +0200 |
paulson |
simpler SELECT_GOAL no longer inserts a dummy parameter
|
file |
diff |
annotate
|
| Tue, 14 Jul 1998 13:31:55 +0200 |
paulson |
CHANGED_GOAL added to declare a more robust stac
|
file |
diff |
annotate
|
| Thu, 05 Feb 1998 11:19:51 +0100 |
wenzelm |
added THEN_ALL_NEW;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:13:21 +0200 |
wenzelm |
ProtoPure.thy;
|
file |
diff |
annotate
|
| Thu, 11 Sep 1997 16:16:03 +0200 |
wenzelm |
removed print_goals_ref (which was broken anyway);
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 11:48:59 +0200 |
paulson |
Removal of tactical STATE
|
file |
diff |
annotate
|
| Tue, 18 Mar 1997 15:15:01 +0100 |
paulson |
A more explicit prefix because gensym now generates easily predicatable
|
file |
diff |
annotate
|
| Fri, 21 Feb 1997 15:31:47 +0100 |
paulson |
Replaced "flat" by the Basis Library function List.concat
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 16:05:07 +0100 |
oheimb |
added THEN_MAYBE and THEN_MAYBE'
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 10:54:16 +0100 |
paulson |
Converted I/O operatios for Basis Library compatibility
|
file |
diff |
annotate
|
| Mon, 04 Nov 1996 10:56:15 +0100 |
paulson |
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
|
file |
diff |
annotate
|
| Mon, 23 Sep 1996 17:46:12 +0200 |
paulson |
Optimized version of SELECT_GOAL, up to 10% faster
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 12:58:47 +0200 |
paulson |
Fixed error in CHANGED (caused by variable renaming)
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 18:39:08 +0100 |
paulson |
Search tacticals moved to search.ML
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:57:32 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Tue, 22 Nov 1994 23:32:16 +0100 |
lcp |
Pure/tctical/protect_subgoal: simplified to use Sequence.hd
|
file |
diff |
annotate
|