1997-11-10 oheimb 1997-11-10 polished definition of find_index_eq
1997-11-10 wenzelm 1997-11-10 check files for non-ASCII characters;
1997-11-10 oheimb 1997-11-10 replaced 8bit characters
1997-11-10 wenzelm 1997-11-10 fixed LAM<...> syntax;
1997-11-10 wenzelm 1997-11-10 fixed spelling;
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it
1997-11-07 oheimb 1997-11-07 added contrapos
1997-11-07 oheimb 1997-11-07 added contrapos2
1997-11-07 oheimb 1997-11-07 added exists_Const
1997-11-07 nipkow 1997-11-07 Each datatype t now proves a theorem split_t_case_prem P(t_case f1 ... fn x) = (~((? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) | ... (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) ) )
1997-11-06 wenzelm 1997-11-06 Perl no longer optional;
1997-11-06 wenzelm 1997-11-06 deriv: eliminated references to theory;
1997-11-06 wenzelm 1997-11-06 tuned;
1997-11-06 wenzelm 1997-11-06 tuned;
1997-11-06 paulson 1997-11-06 hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function
1997-11-06 paulson 1997-11-06 subgoal_tac displays a warning if the new subgoal has type variables
1997-11-05 wenzelm 1997-11-05 mkdir -p bin;
1997-11-05 wenzelm 1997-11-05 Tools/8bit: ./mk;
1997-11-05 oheimb 1997-11-05 *** empty log message ***
1997-11-05 wenzelm 1997-11-05 tuned;
1997-11-05 oheimb 1997-11-05 abandoned generation of tmp files
1997-11-05 oheimb 1997-11-05 various improvements
1997-11-05 oheimb 1997-11-05 reflecting changes of isa2latex
1997-11-05 oheimb 1997-11-05 several minor improvements
1997-11-05 oheimb 1997-11-05 added ax2isa
1997-11-05 oheimb 1997-11-05 added ax2isa
1997-11-05 oheimb 1997-11-05 added isabelle14 and isabelle24
1997-11-05 oheimb 1997-11-05 removed gererated files
1997-11-05 oheimb 1997-11-05 added entry for manual
1997-11-05 oheimb 1997-11-05 *** empty log message ***
1997-11-05 paulson 1997-11-05 Now introduces Safe_tac
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-05 paulson 1997-11-05 Adapted to removal of UN1_I, etc
1997-11-05 paulson 1997-11-05 Adapted to removal of UN1_I, etc
1997-11-05 paulson 1997-11-05 UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
1997-11-05 paulson 1997-11-05 Expandshort; new theorem le_square
1997-11-05 paulson 1997-11-05 generalized UNION1 to UNION
1997-11-05 paulson 1997-11-05 Tidied Key_supply3
1997-11-05 paulson 1997-11-05 fixed comment
1997-11-05 paulson 1997-11-05 UNIV & UNION1
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-05 wenzelm 1997-11-05 adapted typed_print_translation;
1997-11-05 wenzelm 1997-11-05 tuned record_info;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-11-05 wenzelm 1997-11-05 adapted pure_trfunsT; added type_tr/tr'; eliminated mk_ofclassS_tr';
1997-11-05 wenzelm 1997-11-05 print translation: added show_sorts argument;
1997-11-05 wenzelm 1997-11-05 adapted syn_ext_trfunsT;
1997-11-05 wenzelm 1997-11-05 adapted extend_trfunsT;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-11-05 wenzelm 1997-11-05 added TYPE syntax; tuned;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-11-05 wenzelm 1997-11-05 adapted add_trfunsT; defs: admit TYPE arguments;
1997-11-05 wenzelm 1997-11-05 adapted add_trfunsT;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION; added try, can;
1997-11-05 wenzelm 1997-11-05 base root = "";
1997-11-05 nipkow 1997-11-05 Added an alternativ version of AutoChopper and a theory for the conversion of automata into regular sets.
1997-11-04 oheimb 1997-11-04 removed redundant ball_image added image_cong and not_empty added ball and bex of UNIV
1997-11-04 oheimb 1997-11-04 removed redundant ball_empty and bex_empty (see equalities.ML)