src/HOL/Subst/Unify.thy
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2007-10-03 wenzelm 2007-10-03 modernized specifications; tuned proofs;
2007-08-18 wenzelm 2007-08-18 removed obsolete ML bindings;
2007-05-17 krauss 2007-05-17 added pointer to new Unification theory
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2005-04-01 paulson 2005-04-01 x-symbols and other tidying
2005-03-29 paulson 2005-03-29 converted HOL-Subst to tactic scripts
2001-12-06 wenzelm 2001-12-06 use Main;
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
1999-04-22 wenzelm 1999-04-22 recdef requires theory Recdef;
1997-05-22 paulson 1997-05-22 Now uses type option instead of Fail/Subst
1997-05-21 paulson 1997-05-21 Removed rprod from the WF relation
1997-05-15 paulson 1997-05-15 New version, modified by Konrad Slind and LCP for TFL