src/HOL/ex/Unification.thy
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)