History log of /seL4-l4v-master/isabelle/src/HOL/Bali/Value.thy
Revision Date Author Comments
# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# d9ef7419 02-Jan-2016 wenzelm <none@none>

isabelle update_cartouches -c -t;


# c6877bda 02-Nov-2014 wenzelm <none@none>

modernized header;


# 5fc26177 11-Sep-2014 blanchet <none@none>

updated news


# d2ddb3a1 09-Sep-2014 blanchet <none@none>

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries


# 3ec8ee77 18-Feb-2011 wenzelm <none@none>

modernized specifications;


# 9d68725b 26-Jul-2010 wenzelm <none@none>

modernized/unified some specifications;


# 6bc0017f 02-Mar-2010 wenzelm <none@none>

cleanup type translations;


# e9e35adb 09-Feb-2010 wenzelm <none@none>

removed obsolete CVS Ids;


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

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


# bacf0c7b 28-Aug-2005 wenzelm <none@none>

removed obsolete arities;


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

migrated theory headers to new format


# 33b1b845 21-Jun-2004 kleing <none@none>

Merged in license change from Isabelle2004


# c4a5cd8d 31-Oct-2002 schirmer <none@none>

"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.


# 2dc32281 28-Jan-2002 wenzelm <none@none>

GPLed;


# 8af5fde7 28-Jan-2002 wenzelm <none@none>

tuned header;


# 77d49ccc 28-Jan-2002 schirmer <none@none>

Isabelle/Bali sources;