| #
a75a30a3 |
|
11-Feb-2015 |
wenzelm <none@none> |
proper context and method setup;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
| #
0e2280bb |
|
27-Apr-2013 |
wenzelm <none@none> |
uniform Proof.context for hyp_subst_tac;
|
| #
7cffb5dd |
|
17-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
| #
640af3b4 |
|
28-Aug-2009 |
wenzelm <none@none> |
eliminated hard tabs;
|
| #
b305563f |
|
09-Jul-2009 |
wenzelm <none@none> |
removed obsolete CVS Ids;
|
| #
fcd0176f |
|
26-Nov-2006 |
wenzelm <none@none> |
converted legacy ML scripts;
|
| #
347ce55a |
|
20-Sep-2005 |
haftmann <none@none> |
slight adaptions to library changes
|
| #
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
| #
e474f341 |
|
27-Jul-1998 |
paulson <none@none> |
A little quantifier duplication for IFOL
|
| #
81a07728 |
|
19-Dec-1997 |
wenzelm <none@none> |
adapted to new sort function;
|
| #
8b74b342 |
|
09-Feb-1997 |
paulson <none@none> |
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
with Basis Library structure Int
|
| #
8215dc00 |
|
31-Jan-1997 |
paulson <none@none> |
ex_impE was incorrectly listed as Safe
|
| #
8a318c3f |
|
29-Jan-1996 |
clasohm <none@none> |
expanded tabs
|
| #
6581aa17 |
|
06-Apr-1995 |
lcp <none@none> |
Updated comments.
|
| #
22184240 |
|
11-Nov-1994 |
lcp <none@none> |
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|