src/HOL/ex/Unification.thy
2011-08-23 wenzelm 2011-08-23 fixed document;
2011-08-21 krauss 2011-08-21 removed technical or trivial unused facts
2011-08-21 krauss 2011-08-21 more precise authors and comments; tuned order and headers
2011-08-21 krauss 2011-08-21 added proof of idempotence, roughly after HOL/Subst/Unify.thy
2011-08-21 krauss 2011-08-21 tuned proofs, sledgehammering overly verbose parts
2011-08-21 krauss 2011-08-21 tuned notation
2011-08-21 krauss 2011-08-21 ported some lemmas from HOL/Subst/*; tuned order
2011-08-21 krauss 2011-08-21 changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2011-01-07 bulwahn 2011-01-07 removing obselete Id comments from HOL/ex theories
2010-09-28 krauss 2010-09-28 no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-04-21 krauss 2009-04-21 tuned proof
2007-08-28 wenzelm 2007-08-28 induct: proper separation of initial and terminal step; avoid unspecific prems;
2007-07-11 berghofe 2007-07-11 Renamed accessible part for predicates to accp.
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-03 wenzelm 2007-06-03 tuned document;
2007-05-19 haftmann 2007-05-19 fixed text
2007-05-17 krauss 2007-05-17 Added unification case study (using new function package)