1997-05-06 wenzelm 1997-05-06 tuned;
1997-05-06 wenzelm 1997-05-06 *** empty log message ***
1997-05-06 wenzelm 1997-05-06 tuned comments;
1997-05-06 wenzelm 1997-05-06 fixed simplifier ex;
1997-05-06 wenzelm 1997-05-06 SYNC;
1997-05-06 wenzelm 1997-05-06 fixed simplifier examples;
1997-05-06 nipkow 1997-05-06 Stupid bug in induct_tac caused warning to always appear.
1997-05-06 wenzelm 1997-05-06 removed MLtrans, MLtext;
1997-05-06 wenzelm 1997-05-06 added \Pure, \CPure;
1997-05-06 wenzelm 1997-05-06 misc updates, tuning, cleanup;
1997-05-05 wenzelm 1997-05-05 tuned;
1997-05-05 wenzelm 1997-05-05 tuned;
1997-05-05 nipkow 1997-05-05 Cosmetic update of induct_tac; test first now.
1997-05-05 wenzelm 1997-05-05 SYNC;
1997-05-05 wenzelm 1997-05-05 misc updates, tuning, cleanup;
1997-05-05 paulson 1997-05-05 Some blast_tac calls; more needed
1997-05-05 paulson 1997-05-05 Again "norm" DOES NOT normalize bodies of abstractions Showterm (used for tracing) now follows variable instantiations (in order to make up for the "norm" change)
1997-05-02 wenzelm 1997-05-02 fixed comment;
1997-05-02 wenzelm 1997-05-02 -P option (prune empty dirs);
1997-05-02 berghofe 1997-05-02 Updated to LaTeX 2e
1997-05-02 berghofe 1997-05-02 New version of rail.sty for LaTeX 2e
1997-05-02 berghofe 1997-05-02 Updated to LaTeX 2e
1997-05-02 berghofe 1997-05-02 Version of the proof macros for LaTeX 2e
1997-05-02 berghofe 1997-05-02 This file is now replaced by proof.sty
1997-05-02 paulson 1997-05-02 Higher bound means much faster proof
1997-05-02 paulson 1997-05-02 More tracing. hyp_subst_tac allowed to fail
1997-05-02 paulson 1997-05-02 New blast_tac call: made possible by bug fix involving equality substitution
1997-05-01 paulson 1997-05-01 No longer proves mutual_induct unless it is necessary. Previous version proved it, then threw it away...
1997-04-30 paulson 1997-04-30 Documented blast_tac
1997-04-30 paulson 1997-04-30 Automatic update
1997-04-30 paulson 1997-04-30 Indexing for trace_simp
1997-04-30 paulson 1997-04-30 No longer proves mutual induction rules unless they are needed
1997-04-30 paulson 1997-04-30 Fixed clasets so that blast_tac would work
1997-04-30 paulson 1997-04-30 Now modified for sml/nj 109.27
1997-04-30 paulson 1997-04-30 More tracing; less exception handling
1997-04-30 wenzelm 1997-04-30 improved the space2 glyph;
1997-04-30 mueller 1997-04-30 added IOA (meta theory and ABP, NTP examples);
1997-04-30 mueller 1997-04-30 fixed Id;
1997-04-30 mueller 1997-04-30 removed (most of) IOA (see HOLCF/IOA);
1997-04-30 mueller 1997-04-30 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
1997-04-30 mueller 1997-04-30 moved to .. (see also new version in HOLCF/IOA/meta_theory);
1997-04-30 mueller 1997-04-30 removed -- new version in HOLCF/IOA/NTP;
1997-04-30 mueller 1997-04-30 remove -- new version in HOLCF/IOA/ABP;
1997-04-30 paulson 1997-04-30 New theorems Pow_in_Vfrom and Pow_in_VLimit
1997-04-30 mueller 1997-04-30 Old NTP files now running under the IOA meta theory based on HOLCF;
1997-04-30 mueller 1997-04-30 Old ABP files now running under the IOA meta theory based on HOLCF;
1997-04-30 mueller 1997-04-30 New meta theory for IOA based on HOLCF.
1997-04-30 wenzelm 1997-04-30 improved display of non-ASCII chars;
1997-04-29 wenzelm 1997-04-29 fixed enc_start;
1997-04-29 wenzelm 1997-04-29 deactivated new symbols (not yet printable on xterm, emacs);
1997-04-29 wenzelm 1997-04-29 renamed \<choice> to \<orelse>;
1997-04-29 wenzelm 1997-04-29 added \<orelse> symbols syntax for case;
1997-04-29 wenzelm 1997-04-29 added \<langle>, \<rangle> symbols syntax;
1997-04-29 wenzelm 1997-04-29 added new chars;
1997-04-29 wenzelm 1997-04-29 is_blank: added space2 (160);
1997-04-25 wenzelm 1997-04-25 improved DVI_VIEWER default;
1997-04-25 wenzelm 1997-04-25 improved tmp comment;
1997-04-25 wenzelm 1997-04-25 removed -norc;
1997-04-25 slotosch 1997-04-25 used explcite tactics in instances (since ax_per_trans "loops")
1997-04-25 slotosch 1997-04-25 changed Domain->Dom for SML/NJ