1997-11-12 ago oheimb renamed split_prem_tac to split_asm_tac
1997-11-12 ago oheimb renamed split_prem_tac to split_asm_tac
1997-11-11 ago paulson Fixed indentation
1997-11-11 ago paulson Rationalized the theorem if_image_distrib.
1997-11-11 ago paulson Fixed indentation
1997-11-11 ago paulson Fixed spelling error
1997-11-11 ago paulson Made some proofs more robust
1997-11-11 ago paulson Now applies "map negOfGoal" to lits when expanding haz rules.
1997-11-10 ago wenzelm ASCII-fied;
1997-11-10 ago oheimb polished definition of find_index_eq
1997-11-10 ago wenzelm check files for non-ASCII characters;
1997-11-10 ago oheimb replaced 8bit characters
1997-11-10 ago wenzelm fixed LAM<...> syntax;
1997-11-10 ago wenzelm fixed spelling;
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;