TFL/rules.new.sml
1997-08-06 wenzelm 1997-08-06 prs instead of TextIO.output;
1997-07-23 wenzelm 1997-07-23 tmp fix to accomodate rep_ss changes;
1997-06-05 paulson 1997-06-05 Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)
1997-06-03 paulson 1997-06-03 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim)
1997-05-30 paulson 1997-05-30 Simplified the calling sequence of CONTEXT_REWRITE_RULE Eliminated get_rhs, which was calling dest_Trueprop too many times
1997-05-27 paulson 1997-05-27 Removal of module Mask and datatype binding with its constructor |->
1997-05-26 paulson 1997-05-26 More de-HOL-ification
1997-05-22 paulson 1997-05-22 New headers and other minor changes
1997-05-21 paulson 1997-05-21 Basis library input/output primitives; \!simpset instead of HOL_ss
1997-05-20 paulson 1997-05-20 Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable
1997-05-15 paulson 1997-05-15 TFL now integrated with HOL (more work needed)
1997-01-03 paulson 1997-01-03 Conversion to Basis Library (using prs instead of output)
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL