src/HOL/UNITY/Comp/Progress.thy
Thu, 22 Jul 2010 18:08:39 +0200 wenzelm updated some headers;
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Fri, 21 Nov 2008 13:17:43 +0100 paulson Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
Thu, 20 Nov 2008 19:43:34 +0100 wenzelm reactivated some dead theories (based on hints by Mark Hillebrand);
less more (0) -4 tip