src/Pure/section_utils.ML
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1998-12-28 paulson 1998-12-28 deleted "escape" and "trim"; Basis Library can do string escapes if necessary
1998-05-18 wenzelm 1998-05-18 Symbol.stopper;
1998-04-29 wenzelm 1998-04-29 moved mk_defpair to logic.ML; moved get_def to thm.ML; moved require_thy to theory.ML;
1998-03-09 wenzelm 1998-03-09 adapted to new scanners and baroque chars;
1997-10-23 wenzelm 1997-10-23 Sign.stamp_names_of;
1997-10-20 wenzelm 1997-10-20 Sign.base_name;
1997-07-18 wenzelm 1997-07-18 tuned error propagation msg;
1997-04-02 paulson 1997-04-02 Made the error message more explicit
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-08 paulson 1995-12-08 Commented and renamed vars in readtm
1994-10-25 wenzelm 1994-10-25 added require_thy;
1994-09-14 wenzelm 1994-09-14 removed lookup_const (use Sign.const_type instead);
1994-08-25 lcp 1994-08-25 new file of useful things for writing theory sections