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

isabelle update_cartouches -c -t;


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

modernized header uniformly as section;


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

tuned proofs;


# deac04eb 22-Jul-2010 wenzelm <none@none>

updated some headers;


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

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


# d68fbf38 21-Nov-2008 paulson <none@none>

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.


# f766b6ec 20-Nov-2008 wenzelm <none@none>

reactivated some dead theories (based on hints by Mark Hillebrand);


# 3a22d7a5 03-Jan-2006 paulson <none@none>

added explicit paths to required theories


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

migrated theory headers to new format


# 737fdea6 02-Jun-2005 paulson <none@none>

renamed "constrains" to "safety" to avoid keyword clash


# 64b1b57f 17-Mar-2003 paulson <none@none>

More "progress set" material


# 048181da 06-Mar-2003 paulson <none@none>

new UNITY examples theory


# 46ae0aee 05-Mar-2003 paulson <none@none>

new examples theory