Wed, 12 Nov 1997 12:24:55 +0100 |
oheimb |
renamed split_T_case_prem to split_T_case_asm
|
changeset |
files
|
Wed, 12 Nov 1997 12:23:37 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
changeset |
files
|
Wed, 12 Nov 1997 12:22:56 +0100 |
oheimb |
renamed split_prem_tac to split_asm_tac
|
changeset |
files
|
Tue, 11 Nov 1997 16:04:14 +0100 |
paulson |
Fixed indentation
|
changeset |
files
|
Tue, 11 Nov 1997 15:45:56 +0100 |
paulson |
Rationalized the theorem if_image_distrib.
|
changeset |
files
|
Tue, 11 Nov 1997 12:30:51 +0100 |
paulson |
Fixed indentation
|
changeset |
files
|
Tue, 11 Nov 1997 11:16:18 +0100 |
paulson |
Fixed spelling error
|
changeset |
files
|
Tue, 11 Nov 1997 11:15:51 +0100 |
paulson |
Made some proofs more robust
|
changeset |
files
|
Tue, 11 Nov 1997 11:12:37 +0100 |
paulson |
Now applies "map negOfGoal" to lits when expanding haz rules.
|
changeset |
files
|
Mon, 10 Nov 1997 15:25:12 +0100 |
wenzelm |
ASCII-fied;
|
changeset |
files
|
Mon, 10 Nov 1997 15:06:58 +0100 |
oheimb |
polished definition of find_index_eq
|
changeset |
files
|
Mon, 10 Nov 1997 15:05:41 +0100 |
wenzelm |
check files for non-ASCII characters;
|
changeset |
files
|
Mon, 10 Nov 1997 14:57:31 +0100 |
oheimb |
replaced 8bit characters
|
changeset |
files
|
Mon, 10 Nov 1997 14:30:35 +0100 |
wenzelm |
fixed LAM<...> syntax;
|
changeset |
files
|
Mon, 10 Nov 1997 11:47:32 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
Fri, 07 Nov 1997 18:05:25 +0100 |
oheimb |
added split_prem_tac
|
changeset |
files
|
Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
changeset |
files
|
Fri, 07 Nov 1997 17:51:26 +0100 |
oheimb |
added contrapos
|
changeset |
files
|
Fri, 07 Nov 1997 17:51:10 +0100 |
oheimb |
added contrapos2
|
changeset |
files
|
Fri, 07 Nov 1997 15:24:58 +0100 |
oheimb |
added exists_Const
|
changeset |
files
|
Fri, 07 Nov 1997 08:25:02 +0100 |
nipkow |
Each datatype t now proves a theorem split_t_case_prem
|
changeset |
files
|
Thu, 06 Nov 1997 16:44:35 +0100 |
wenzelm |
Perl no longer optional;
|
changeset |
files
|
Thu, 06 Nov 1997 16:41:08 +0100 |
wenzelm |
deriv: eliminated references to theory;
|
changeset |
files
|
Thu, 06 Nov 1997 16:40:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 Nov 1997 12:27:12 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 Nov 1997 10:29:37 +0100 |
paulson |
hyp_subst_tac checks if the equality has type variables and uses a suitable
|
changeset |
files
|
Thu, 06 Nov 1997 10:28:20 +0100 |
paulson |
subgoal_tac displays a warning if the new subgoal has type variables
|
changeset |
files
|
Wed, 05 Nov 1997 19:40:50 +0100 |
wenzelm |
mkdir -p bin;
|
changeset |
files
|
Wed, 05 Nov 1997 19:39:34 +0100 |
wenzelm |
Tools/8bit: ./mk;
|
changeset |
files
|
Wed, 05 Nov 1997 18:31:14 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|