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
|
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
|
Wed, 05 Nov 1997 13:26:19 +0100 |
paulson |
fixed comment
|
changeset |
files
|
Wed, 05 Nov 1997 13:25:34 +0100 |
paulson |
UNIV & UNION1
|
changeset |
files
|
Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
Wed, 05 Nov 1997 13:14:15 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
changeset |
files
|
Wed, 05 Nov 1997 11:49:34 +0100 |
wenzelm |
adapted typed_print_translation;
|
changeset |
files
|
Wed, 05 Nov 1997 11:49:07 +0100 |
wenzelm |
tuned record_info;
|
changeset |
files
|
Wed, 05 Nov 1997 11:45:51 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
Wed, 05 Nov 1997 11:43:37 +0100 |
wenzelm |
adapted pure_trfunsT;
|
changeset |
files
|
Wed, 05 Nov 1997 11:42:19 +0100 |
wenzelm |
print translation: added show_sorts argument;
|
changeset |
files
|
Wed, 05 Nov 1997 11:41:46 +0100 |
wenzelm |
adapted syn_ext_trfunsT;
|
changeset |
files
|
Wed, 05 Nov 1997 11:41:18 +0100 |
wenzelm |
adapted extend_trfunsT;
|
changeset |
files
|
Wed, 05 Nov 1997 11:40:51 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
Wed, 05 Nov 1997 11:40:23 +0100 |
wenzelm |
added TYPE syntax;
|
changeset |
files
|
Wed, 05 Nov 1997 11:35:07 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
Wed, 05 Nov 1997 11:34:44 +0100 |
wenzelm |
adapted add_trfunsT;
|
changeset |
files
|
Wed, 05 Nov 1997 11:33:45 +0100 |
wenzelm |
adapted add_trfunsT;
|
changeset |
files
|
Wed, 05 Nov 1997 11:33:05 +0100 |
wenzelm |
fixed exception OPTION;
|
changeset |
files
|
Wed, 05 Nov 1997 11:19:15 +0100 |
wenzelm |
base root = "";
|
changeset |
files
|
Wed, 05 Nov 1997 09:08:35 +0100 |
nipkow |
Added an alternativ version of AutoChopper and a theory for the conversion of
|
changeset |
files
|
Tue, 04 Nov 1997 20:52:20 +0100 |
oheimb |
removed redundant ball_image
|
changeset |
files
|