History log of /seL4-l4v-master/isabelle/src/HOL/UNITY/Guar.thy
Revision Date Author Comments
# 09859749 18-Nov-2018 haftmann <none@none>

removed legacy input syntax


# f5796e6d 14-Feb-2018 wenzelm <none@none>

more symbols;


# ef344a77 25-May-2016 wenzelm <none@none>

isabelle update_cartouches -c -t;


# 6fc0f068 28-Dec-2015 wenzelm <none@none>

prefer symbols for "Union", "Inter";


# 5012105f 13-Sep-2015 wenzelm <none@none>

tuned proofs -- less legacy;


# f67d856d 25-Mar-2015 wenzelm <none@none>

prefer local fixes;


# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;


# dc6cdd46 21-Feb-2012 wenzelm <none@none>

tuned proofs;


# 6337ab39 12-Nov-2011 wenzelm <none@none>

tuned proofs;


# 335fd006 10-Sep-2011 wenzelm <none@none>

misc tuning and clarification;


# baea5702 01-Mar-2010 haftmann <none@none>

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)


# 079cde2d 17-Oct-2009 wenzelm <none@none>

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;


# a84018cb 24-Jul-2008 haftmann <none@none>

added class preorder


# 46a1ad78 01-Jul-2005 berghofe <none@none>

Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.


# a7060872 17-Jun-2005 haftmann <none@none>

migrated theory headers to new format


# 402829d8 15-Jul-2003 paulson <none@none>

tidying


# 3c4494d5 15-Feb-2003 paulson <none@none>

minor revisions


# 5bb51f23 08-Feb-2003 paulson <none@none>

converting HOL/UNITY to use unconditional fairness


# 2380b71a 04-Feb-2003 paulson <none@none>

some x-symbols


# 1674bc09 31-Jan-2003 paulson <none@none>

conversion to new-style theories and tidying


# b4eac3e6 29-Jan-2003 paulson <none@none>

converted more UNITY theories to new-style


# 543684e4 01-Dec-2001 wenzelm <none@none>

renamed class "term" to "type" (actually "HOL.type");


# 20030c6d 02-Mar-2001 ehmety <none@none>

*** empty log message ***


# ced4250f 23-Sep-2000 paulson <none@none>

added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.


# 31503020 14-Jul-2000 paulson <none@none>

used bounded quantification in definition of guarantees and other minor
adjustments


# af066af4 08-Dec-1999 paulson <none@none>

abolition of localTo: instead "guarantees" has local vars as extra argument


# fc68c146 31-Aug-1999 paulson <none@none>

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