src/HOL/Statespace/distinct_tree_prover.ML
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-11-06 wenzelm 2011-11-06 inlined antiquotations;
2011-11-06 wenzelm 2011-11-06 misc tuning and modernization;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
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