1997-11-07 ago oheimb added split_prem_tac
1997-11-07 ago oheimb changed libraray function find to find_index_eq, currying it
1997-11-07 ago oheimb added contrapos
1997-11-07 ago oheimb added contrapos2
1997-11-07 ago oheimb added exists_Const
1997-11-07 ago nipkow Each datatype t now proves a theorem split_t_case_prem
1997-11-06 ago wenzelm Perl no longer optional;
1997-11-06 ago wenzelm deriv: eliminated references to theory;
1997-11-06 ago wenzelm tuned;
1997-11-06 ago wenzelm tuned;
1997-11-06 ago paulson hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-11-06 ago paulson subgoal_tac displays a warning if the new subgoal has type variables
1997-11-05 ago wenzelm mkdir -p bin;
1997-11-05 ago wenzelm Tools/8bit: ./mk;
1997-11-05 ago oheimb *** empty log message ***
1997-11-05 ago wenzelm tuned;
1997-11-05 ago oheimb abandoned generation of tmp files
1997-11-05 ago oheimb various improvements
1997-11-05 ago oheimb reflecting changes of isa2latex
1997-11-05 ago oheimb several minor improvements
1997-11-05 ago oheimb added ax2isa
1997-11-05 ago oheimb added ax2isa
1997-11-05 ago oheimb added isabelle14 and isabelle24
1997-11-05 ago oheimb removed gererated files
1997-11-05 ago oheimb added entry for manual
1997-11-05 ago oheimb *** empty log message ***
1997-11-05 ago paulson Now introduces Safe_tac
1997-11-05 ago paulson Ran expandshort, especially to introduce Safe_tac
1997-11-05 ago paulson Adapted to removal of UN1_I, etc
1997-11-05 ago paulson Adapted to removal of UN1_I, etc
1997-11-05 ago paulson UNIV now a constant; UNION1, INTER1 now translations and no longer have
1997-11-05 ago paulson Expandshort; new theorem le_square
1997-11-05 ago paulson generalized UNION1 to UNION
1997-11-05 ago paulson Tidied Key_supply3
1997-11-05 ago paulson fixed comment
1997-11-05 ago paulson UNIV & UNION1
1997-11-05 ago paulson Ran expandshort, especially to introduce Safe_tac
1997-11-05 ago paulson Ran expandshort, especially to introduce Safe_tac
1997-11-05 ago wenzelm adapted typed_print_translation;
1997-11-05 ago wenzelm tuned record_info;
1997-11-05 ago wenzelm fixed exception OPTION;
1997-11-05 ago wenzelm adapted pure_trfunsT;
1997-11-05 ago wenzelm print translation: added show_sorts argument;
1997-11-05 ago wenzelm adapted syn_ext_trfunsT;
1997-11-05 ago wenzelm adapted extend_trfunsT;
1997-11-05 ago wenzelm fixed exception OPTION;
1997-11-05 ago wenzelm added TYPE syntax;
1997-11-05 ago wenzelm fixed exception OPTION;
1997-11-05 ago wenzelm adapted add_trfunsT;
1997-11-05 ago wenzelm adapted add_trfunsT;
1997-11-05 ago wenzelm fixed exception OPTION;
1997-11-05 ago wenzelm base root = "";
1997-11-05 ago nipkow Added an alternativ version of AutoChopper and a theory for the conversion of
1997-11-04 ago oheimb removed redundant ball_image
1997-11-04 ago oheimb removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-04 ago oheimb added several theorems
1997-11-04 ago oheimb added the, option_map, and case analysis theorems
1997-11-04 ago oheimb added zip and nodup
1997-11-04 ago oheimb added theorems for Eps
1997-11-04 ago wenzelm tuned usage;