1997-03-11 wenzelm 1997-03-11 added THIS_IS_ISABELLE_BUILD;
1997-03-11 wenzelm 1997-03-11 added THIS_IS_ISABELLE_BUILD discrimination;
1997-03-10 paulson 1997-03-10 The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac does not recognize eta-equality. But making it do so is costly
1997-03-07 wenzelm 1997-03-07 renamed;
1997-03-07 wenzelm 1997-03-07 fixed;
1997-03-07 wenzelm 1997-03-07 commented out chwon, chmod;
1997-03-07 wenzelm 1997-03-07 fixed src path;
1997-03-07 wenzelm 1997-03-07 added \n at EOF;
1997-03-07 wenzelm 1997-03-07 *** empty log message ***
1997-03-07 wenzelm 1997-03-07 tuned;
1997-03-07 wenzelm 1997-03-07 renamed fonts;
1997-03-07 wenzelm 1997-03-07 renamed font;
1997-03-07 wenzelm 1997-03-07 removed lparr, rparr, empty, succeq, ge, rrightarrow; added turnstile, Turnstile, cdot, approx, Colon, bow; renamed tick to surd;
1997-03-07 wenzelm 1997-03-07 renamed SYSTEM to RAW_ML_SYSTEM;
1997-03-07 wenzelm 1997-03-07 added \<Colon> syntax for constraints (more compact!);
1997-03-07 wenzelm 1997-03-07 "bool lift" now syntax instead of type abbrev;
1997-03-07 wenzelm 1997-03-07 *** empty log message ***
1997-03-07 wenzelm 1997-03-07 added atac 2 (again);
1997-03-07 wenzelm 1997-03-07 removed (| |) symbols syntax;
1997-03-07 wenzelm 1997-03-07 fixed Not syntax;
1997-03-07 wenzelm 1997-03-07 tuned comment;
1997-03-07 wenzelm 1997-03-07 tuned comments;
1997-03-07 wenzelm 1997-03-07 Isabelle installation notes;
1997-03-07 wenzelm 1997-03-07 now sans serifs;
1997-03-07 wenzelm 1997-03-07 tuned;
1997-03-07 wenzelm 1997-03-07 *** empty log message ***
1997-03-07 wenzelm 1997-03-07 build - compile parts of the Isabelle system;
1997-03-07 wenzelm 1997-03-07 moved settings comment to build;
1997-03-07 paulson 1997-03-07 Removed some polymorphic equality tests
1997-03-07 paulson 1997-03-07 Improved indentation of aconv
1997-03-07 paulson 1997-03-07 Corrected aeconv and exported it
1997-03-07 paulson 1997-03-07 Prevent permutation of assumptions in hyp_subst_tac
1997-03-07 paulson 1997-03-07 Deleted steps made redundant by the stronger eq_assume_tac
1997-03-07 paulson 1997-03-07 Eta-expanded some declarations for compatibility with value polymorphism
1997-03-07 paulson 1997-03-07 Tidied and updated
1997-03-07 wenzelm 1997-03-07 more robust check;
1997-03-07 wenzelm 1997-03-07 renamed, improved, augmented version of isabelle fonts;
1997-03-07 wenzelm 1997-03-07 tuned comment;
1997-03-07 wenzelm 1997-03-07 tuned;
1997-03-07 wenzelm 1997-03-07 pass xterm mode by default;
1997-03-06 pusch 1997-03-06 Minor changes due to primrec definition for ^
1997-03-06 pusch 1997-03-06 primrec definition for ^
1997-03-06 pusch 1997-03-06 Minor changes due to primrec definition for nth
1997-03-06 pusch 1997-03-06 primrec definition for nth
1997-03-06 wenzelm 1997-03-06 Oops, forgot to remove -x again;
1997-03-06 wenzelm 1997-03-06 added ISABELLE_HOME normalization;
1997-03-06 wenzelm 1997-03-06 even more robust and user friendly invocation (no longer requieres absolute path names);
1997-03-05 wenzelm 1997-03-05 improved DESCRIPTION;
1997-03-05 wenzelm 1997-03-05 added -a, -b options; multiple VARNAMES;
1997-03-05 wenzelm 1997-03-05 *** empty log message ***
1997-03-05 wenzelm 1997-03-05 *** empty log message ***
1997-03-05 wenzelm 1997-03-05 *** empty log message ***
1997-03-05 paulson 1997-03-05 Added comment
1997-03-05 paulson 1997-03-05 Now uses eta_contract_atom for greater speed
1997-03-05 paulson 1997-03-05 Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-03-05 paulson 1997-03-05 HOL: renaming of "not"
1997-03-05 paulson 1997-03-05 Declares eta_contract_atom; fixed comment; some tidying
1997-03-05 paulson 1997-03-05 Added comment
1997-03-05 paulson 1997-03-05 Now declares needs_filtered_use, but still unusable with current MLWorks
1997-03-05 paulson 1997-03-05 Now uses rotate_tac and eta_contract_atom for greater speed