src/HOL/UNITY/Guar.thy
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2012-02-21 wenzelm 2012-02-21 tuned proofs;
2011-11-12 wenzelm 2011-11-12 tuned proofs;
2011-09-10 wenzelm 2011-09-10 misc tuning and clarification;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2008-07-25 haftmann 2008-07-25 added class preorder
2005-07-01 berghofe 2005-07-01 Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-07-15 paulson 2003-07-15 tidying
2003-02-16 paulson 2003-02-16 minor revisions
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-02-04 paulson 2003-02-04 some x-symbols
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-29 paulson 2003-01-29 converted more UNITY theories to new-style
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-03-02 ehmety 2001-03-02 *** empty log message ***
2000-09-23 paulson 2000-09-23 added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
2000-07-14 paulson 2000-07-14 used bounded quantification in definition of guarantees and other minor adjustments
1999-12-08 paulson 1999-12-08 abolition of localTo: instead "guarantees" has local vars as extra argument
1999-08-31 paulson 1999-08-31 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants