1997-11-16 nipkow 1997-11-16 Removed "(ALL x:f``A. P x) = (ALL x:A. P(f x))", "(EX x:f``A. P x) = (EX x:A. P(f x))", again, because they were already there and added "(UN x:f``A. B x) = (UN a:A. B(f a))" "(INT x:f``A. B x) = (INT a:A. B(f a))" instead.
1997-11-15 nipkow 1997-11-15 Redesigned the decision procedures for (Abelian) groups and commutative rings.
1997-11-15 nipkow 1997-11-15 Added > "(? x : f `` A. P x) = (? a:A. P(f a))" > "(! x : f `` A. P x) = (! a:A. P(f a))"
1997-11-14 wenzelm 1997-11-14 merge_refs: check for different versions of theories;
1997-11-13 wenzelm 1997-11-13 export read_raw_typ;
1997-11-13 wenzelm 1997-11-13 fixed record parser;
1997-11-13 wenzelm 1997-11-13 improved record syntax;
1997-11-13 wenzelm 1997-11-13 made SML/NJ happy;
1997-11-12 oheimb 1997-11-12 added thin_refl to hyp_subst_tac
1997-11-12 wenzelm 1997-11-12 refer to $ISABELLE_HOME/src;
1997-11-12 wenzelm 1997-11-12 structure BasisLibrary;
1997-11-12 wenzelm 1997-11-12 renamed to use.ML;
1997-11-12 wenzelm 1997-11-12 Redefine 'use' command in order to support path variable expansion, automatic suffix generation, and symbolic input filtering (if required).
1997-11-12 wenzelm 1997-11-12 adapted to new Use, File structs;
1997-11-12 wenzelm 1997-11-12 added path variables;
1997-11-12 wenzelm 1997-11-12 File system operations.
1997-11-12 wenzelm 1997-11-12 moved old file stuff from library.ML to Thy/browser_info.ML; subdir_of no longer infix;
1997-11-12 wenzelm 1997-11-12 added file.ML, use.ML; removed symbol_input.ML;
1997-11-12 wenzelm 1997-11-12 tuned warning msg;
1997-11-12 wenzelm 1997-11-12 major cleanup; removed several obsolete functions; moved file stuff to Thy/file.ML;
1997-11-12 wenzelm 1997-11-12 moved 'latex' from library.ML to goals.ML;
1997-11-12 wenzelm 1997-11-12 tuned prths;
1997-11-12 wenzelm 1997-11-12 structure BasisLibrary;
1997-11-12 wenzelm 1997-11-12 added Thy/file.ML, Thy/use.ML; removed Thy/symbol_input.ML;
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac
1997-11-12 oheimb 1997-11-12 restored last version
1997-11-12 oheimb 1997-11-12 simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm cladata.ML: unintentinally committed
1997-11-12 oheimb 1997-11-12 renamed split_T_case_prem to split_T_case_asm
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac split_asm_tac: simplification, debugged first_prem_is_disj
1997-11-11 paulson 1997-11-11 Fixed indentation
1997-11-11 paulson 1997-11-11 Rationalized the theorem if_image_distrib. Added parens to not_empty.
1997-11-11 paulson 1997-11-11 Fixed indentation
1997-11-11 paulson 1997-11-11 Fixed spelling error
1997-11-11 paulson 1997-11-11 Made some proofs more robust
1997-11-11 paulson 1997-11-11 Now applies "map negOfGoal" to lits when expanding haz rules. Also improved comments
1997-11-10 wenzelm 1997-11-10 ASCII-fied;
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