TFL/usyntax.sml
2000-09-06 wenzelm 2000-09-06 tuned;
2000-09-05 wenzelm 2000-09-05 tuned;
2000-07-16 wenzelm 2000-07-16 strip_prod_type = HOLogic.prodT_factors;
2000-05-18 wenzelm 2000-05-18 fewer consts declared as global;
1999-04-23 paulson 1999-04-23 Now for recdefs that omit the WF relation; removed the separation between draft and theory modes
1997-09-25 paulson 1997-09-25 Deleted the unused list_mk_disj
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-27 paulson 1997-05-27 Removal of module Mask and datatype binding with its constructor |->
1997-05-26 paulson 1997-05-26 Deleted unused functions
1997-05-22 paulson 1997-05-22 New headers and other minor changes
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
1996-10-18 paulson 1996-10-18 Konrad Slind's TFL