History log of /seL4-l4v-10.1.1/isabelle/src/HOL/UNITY/Comp.thy
Revision Date Author Comments
# ef344a77 25-May-2016 wenzelm <none@none>

isabelle update_cartouches -c -t;


# c9f3da2d 27-Dec-2015 wenzelm <none@none>

discontinued ASCII replacement syntax <->;


# 18551fee 13-Oct-2015 haftmann <none@none>

prod_case as canonical name for product type eliminator


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

prefer local fixes;


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

modernized header uniformly as section;


# 7f9cbadc 13-Mar-2012 wenzelm <none@none>

tuned context specifications and proofs;


# 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;


# 39f27693 20-Apr-2009 haftmann <none@none>

power operation on functions with syntax o^; power operation on relations with syntax ^^


# 99b04075 03-Aug-2007 wenzelm <none@none>

misc cleanup of ML bindings (for multihreading);


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

migrated theory headers to new format


# 23566625 27-May-2003 paulson <none@none>

removed redundant line


# 14459920 21-Mar-2003 paulson <none@none>

More on progress sets


# 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 ***


# 07f81ce6 13-Jan-2000 paulson <none@none>

still working; a bit of polishing


# 808483ad 13-Jan-2000 paulson <none@none>

working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.


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

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


# 19656c80 31-Aug-1999 paulson <none@none>

changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <


# 3a0e1fa8 26-Aug-1999 paulson <none@none>

changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE


# 0fc2c95f 13-Jun-1999 paulson <none@none>

guarantees -> guar


# e18f862e 17-May-1999 paulson <none@none>

"component" now an infix


# a6490db6 01-Mar-1999 paulson <none@none>

removed the infernal States, eqStates, compatible, etc.


# 67c1e3a6 19-Jan-1999 paulson <none@none>

updated comments


# 76d0cd85 03-Dec-1998 paulson <none@none>

Addition of the States component; parts of Comp not working


# b24603b6 05-Oct-1998 paulson <none@none>

Finished proofs to end of section 5.1 of Chandy and Sanders


# 05b861d6 01-Oct-1998 paulson <none@none>

composition theory