src/HOL/ex/Unification.thy
Tue, 23 Aug 2011 17:44:31 +0200 wenzelm fixed document;
Sun, 21 Aug 2011 22:13:04 +0200 krauss removed technical or trivial unused facts
Sun, 21 Aug 2011 22:13:04 +0200 krauss more precise authors and comments;
Sun, 21 Aug 2011 22:13:04 +0200 krauss added proof of idempotence, roughly after HOL/Subst/Unify.thy
Sun, 21 Aug 2011 22:13:04 +0200 krauss tuned proofs, sledgehammering overly verbose parts
Sun, 21 Aug 2011 22:13:04 +0200 krauss tuned notation
Sun, 21 Aug 2011 22:13:04 +0200 krauss ported some lemmas from HOL/Subst/*;
Sun, 21 Aug 2011 22:13:04 +0200 krauss changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
Sat, 23 Apr 2011 13:00:19 +0200 wenzelm modernized specifications;
Fri, 07 Jan 2011 14:46:28 +0100 bulwahn removing obselete Id comments from HOL/ex theories
Tue, 28 Sep 2010 09:54:07 +0200 krauss no longer declare .psimps rules as [simp].
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 21 Apr 2009 09:53:31 +0200 krauss tuned proof
Tue, 28 Aug 2007 11:25:29 +0200 wenzelm induct: proper separation of initial and terminal step;
Wed, 11 Jul 2007 11:54:03 +0200 berghofe Renamed accessible part for predicates to accp.
Wed, 13 Jun 2007 18:30:11 +0200 wenzelm tuned proofs: avoid implicit prems;
Sun, 03 Jun 2007 23:16:47 +0200 wenzelm tuned document;
Sat, 19 May 2007 11:33:30 +0200 haftmann fixed text
Thu, 17 May 2007 22:33:41 +0200 krauss Added unification case study (using new function package)
less more (0) tip