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