src/HOL/Statespace/distinct_tree_prover.ML
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-15 wenzelm 2010-05-15 tuned;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-03-05 wenzelm 2009-03-05 removed spurious occurrences of old rep_ss;
2009-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-11-12 schirmer 2007-11-12 added signatures; tuned
2007-10-24 schirmer 2007-10-24 added Statespace library