| Wed, 12 Aug 1998 16:21:18 +0200 |
oheimb |
the splitter is now defined as a functor
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 19:18:50 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 19:02:52 +0200 |
wenzelm |
functorized Clasimp module;
|
file |
diff |
annotate
|
| Thu, 02 Jul 1998 17:56:06 +0200 |
paulson |
HACKED declaration of addsplits
|
file |
diff |
annotate
|
| Thu, 14 May 1998 16:50:09 +0200 |
oheimb |
extended addsplits and delsplits to handle also split rules for assumptions
|
file |
diff |
annotate
|
| Sat, 04 Apr 1998 12:29:07 +0200 |
wenzelm |
no open Simplifier;
|
file |
diff |
annotate
|
| Sat, 28 Feb 1998 15:41:17 +0100 |
nipkow |
Splitters via named loopers.
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 20:25:27 +0100 |
oheimb |
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:45:32 +0100 |
oheimb |
changed wrapper mechanism of classical reasoner
|
file |
diff |
annotate
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 10:48:16 +0100 |
paulson |
Instantiated the one-point-rule quantifier simpprocs for FOL
|
file |
diff |
annotate
|
| Fri, 28 Nov 1997 10:54:13 +0100 |
paulson |
addsplits now in FOL, ZF too
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 12:23:37 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:05:25 +0100 |
oheimb |
added split_prem_tac
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:28:01 +0100 |
wenzelm |
adapted to new implicit simpset;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 10:57:48 +0200 |
paulson |
New simprules imp_disj1,2 and some comments
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 15:52:12 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 00:41:40 +0200 |
berghofe |
Moved functions from file "thy_data.ML".
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 12:54:49 +0200 |
wenzelm |
standard congs;
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:12:55 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Thu, 15 May 1997 15:51:09 +0200 |
oheimb |
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
|
file |
diff |
annotate
|
| Tue, 18 Mar 1997 08:43:26 +0100 |
nipkow |
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
|
file |
diff |
annotate
|
| Wed, 05 Mar 1997 10:07:04 +0100 |
paulson |
Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:43:27 +0100 |
oheimb |
added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
|
file |
diff |
annotate
|
| Mon, 10 Feb 1997 12:31:54 +0100 |
paulson |
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Wed, 09 Oct 1996 13:36:17 +0200 |
paulson |
Added the de Morgan laws (incl quantifier versions) to basic simpset
|
file |
diff |
annotate
|
| Tue, 08 Oct 1996 10:17:50 +0200 |
paulson |
Addition of one-point quantifier rewrite rules
|
file |
diff |
annotate
|
| Mon, 09 Sep 1996 10:59:32 +0200 |
paulson |
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
|
file |
diff |
annotate
|