1996-11-27 paulson 1996-11-27 Updated instructions
1996-11-27 paulson 1996-11-27 Better indentation
1996-11-27 paulson 1996-11-27 Replaced obsolete "use" command
1996-11-27 paulson 1996-11-27 Compatibility with SML/NJ 109, and some compatibility with later versions
1996-11-27 paulson 1996-11-27 Now tries to delete SML/NJ .heap files
1996-11-27 paulson 1996-11-27 Converted I/O operatios for Basis Library compatibility
1996-11-27 paulson 1996-11-27 Eta-expanded some declarations that are illegal under value polymorphism Converted I/O operatios for Basis Library compatibility
1996-11-27 paulson 1996-11-27 Basis library emulation, especially of I/O operations
1996-11-27 paulson 1996-11-27 Removed an obsolete and incompatible declaration
1996-11-27 paulson 1996-11-27 Replaced obsolete "makestring" by Bool.toString
1996-11-27 paulson 1996-11-27 Replaced obsolete "makestring" by Int.toString
1996-11-27 paulson 1996-11-27 Eta-expanded some declarations that are illegal under value polymorphism
1996-11-27 paulson 1996-11-27 Replaced obsolete "use" command
1996-11-27 paulson 1996-11-27 Uses Basis Library equivalent of cd
1996-11-27 paulson 1996-11-27 Makefile improvements by Thomas Santen and Stephan Herrmann Should be more portable across different versions of make
1996-11-26 oheimb 1996-11-26 if_cancel added to HOL_ss
1996-11-26 paulson 1996-11-26 Removed or eta-expanded some declarations that are illegal under value polymorphism
1996-11-26 paulson 1996-11-26 Checks for empty files. Replaces auto() calls
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-26 paulson 1996-11-26 Structure Bool and value Int.toString needed to replace makestring calls
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-26 paulson 1996-11-26 Removal of needless function definition
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
1996-11-26 paulson 1996-11-26 Added instructions on starting up
1996-11-26 paulson 1996-11-26 New material from Norbert Voelker for efficient binary comparisons
1996-11-26 nipkow 1996-11-26 A bit of commutative ing theory, with a simplification tacxtic and an example.
1996-11-26 nipkow 1996-11-26 Added Lagrang. Modified comment.
1996-11-25 nipkow 1996-11-25 Replaced LK&Modal by Sequents
1996-11-22 paulson 1996-11-22 Updating of a reference (Ch. Paulin)
1996-11-22 paulson 1996-11-22 Minor textual improvements; updating of a reference
1996-11-22 paulson 1996-11-22 Have been obsolete for months; contents are now in Shared and NS_Shared
1996-11-22 paulson 1996-11-22 Basis library emulation for old ML compilers
1996-11-21 paulson 1996-11-21 Added warning message
1996-11-21 paulson 1996-11-21 Tidied up some proofs, ...
1996-11-21 paulson 1996-11-21 Minor reformatting
1996-11-21 paulson 1996-11-21 Further comments on versions of SML/NJ
1996-11-20 nipkow 1996-11-20 plus -> Plus to avoid hiding class plus
1996-11-19 wenzelm 1996-11-19 restored changed prettyprinting of ==>;
1996-11-19 wenzelm 1996-11-19 removed old commented out text;
1996-11-19 wenzelm 1996-11-19 minor tuning;
1996-11-19 wenzelm 1996-11-19 tuned some char names;
1996-11-19 wenzelm 1996-11-19 added this file;
1996-11-19 wenzelm 1996-11-19 added add_modesyntax(_i);
1996-11-18 wenzelm 1996-11-18 added symbolfont syntax;
1996-11-18 wenzelm 1996-11-18 improved string scanner: converts 8 bit chars to escape sequences;
1996-11-18 wenzelm 1996-11-18 mixfix: added syntax for Infirl/rName; syntax section: added option printer table name;
1996-11-18 wenzelm 1996-11-18 extend_const_gram now supports multiple disjoint printer tables;
1996-11-18 wenzelm 1996-11-18 new delimiter syntax in mixfixes: \{SYMBOLNAME} is char from symbol font;
1996-11-18 wenzelm 1996-11-18 added print_mode: string list ref (order of printer tables); multiple disjoint printer tables, to be combined hierarchically; multiple entries in printer tables (matched in order);
1996-11-18 wenzelm 1996-11-18 added Infixl/rName: specify infix name independently from syntax; added Pure symbolfont syntax;
1996-11-18 wenzelm 1996-11-18 added symbol_font.ML;
1996-11-18 wenzelm 1996-11-18 added add_modesyntax(_i); improved syntax of ==, =?=, ==> (now allows "op ..."); added Pure symbolfont syntax;
1996-11-18 wenzelm 1996-11-18 added is_printable: string -> bool;
1996-11-18 wenzelm 1996-11-18 added Syntax/symbol_font.ML;
1996-11-18 paulson 1996-11-18 Removal of an obsolete result, and authentication of B to A
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-18 paulson 1996-11-18 Optimizations: removal of polymorphic equality; one-argument case for subst_bounds
1996-11-18 paulson 1996-11-18 Speedups involving norm
1996-11-18 paulson 1996-11-18 Introduction of structure Int