src/HOL/UNITY/Comp/PriorityAux.thy
2014-06-22 nipkow 2014-06-22 r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
2014-06-21 nipkow 2014-06-21 added [simp]
2012-03-13 wenzelm 2012-03-13 tuned proofs;
2011-12-13 wenzelm 2011-12-13 modernized specifications;
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2006-09-19 wenzelm 2006-09-19 removed duplicate arities;
2004-11-08 paulson 2004-11-08 tidied comments
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-07-03 paulson 2003-07-03 converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-03-05 paulson 2001-03-05 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp