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
|
Wed, 05 Nov 1997 16:37:22 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 05 Nov 1997 15:49:38 +0100 |
oheimb |
abandoned generation of tmp files
|
changeset |
files
|
Wed, 05 Nov 1997 15:48:24 +0100 |
oheimb |
various improvements
|
changeset |
files
|
Wed, 05 Nov 1997 15:47:27 +0100 |
oheimb |
reflecting changes of isa2latex
|
changeset |
files
|
Wed, 05 Nov 1997 15:45:51 +0100 |
oheimb |
several minor improvements
|
changeset |
files
|
Wed, 05 Nov 1997 15:42:30 +0100 |
oheimb |
added ax2isa
|
changeset |
files
|
Wed, 05 Nov 1997 15:42:07 +0100 |
oheimb |
added ax2isa
|
changeset |
files
|
Wed, 05 Nov 1997 15:38:40 +0100 |
oheimb |
added isabelle14 and isabelle24
|
changeset |
files
|
Wed, 05 Nov 1997 15:36:54 +0100 |
oheimb |
removed gererated files
|
changeset |
files
|
Wed, 05 Nov 1997 15:36:40 +0100 |
oheimb |
added entry for manual
|
changeset |
files
|
Wed, 05 Nov 1997 15:36:01 +0100 |
oheimb |
*** empty log message ***
|
changeset |
files
|
Wed, 05 Nov 1997 14:00:49 +0100 |
paulson |
Now introduces Safe_tac
|
changeset |
files
|
Wed, 05 Nov 1997 13:50:59 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
Wed, 05 Nov 1997 13:50:16 +0100 |
paulson |
Adapted to removal of UN1_I, etc
|
changeset |
files
|
Wed, 05 Nov 1997 13:45:01 +0100 |
paulson |
Adapted to removal of UN1_I, etc
|
changeset |
files
|
Wed, 05 Nov 1997 13:32:07 +0100 |
paulson |
UNIV now a constant; UNION1, INTER1 now translations and no longer have
|
changeset |
files
|
Wed, 05 Nov 1997 13:29:47 +0100 |
paulson |
Expandshort; new theorem le_square
|
changeset |
files
|
Wed, 05 Nov 1997 13:27:58 +0100 |
paulson |
generalized UNION1 to UNION
|
changeset |
files
|
Wed, 05 Nov 1997 13:27:29 +0100 |
paulson |
Tidied Key_supply3
|
changeset |
files
|