History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Bali/Term.thy
Revision Date Author Comments
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# 35f7dccd 23-Feb-2016 nipkow <none@none>

more canonical names


# 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


# 34dc661e 09-Sep-2014 blanchet <none@none>

ported Bali to new datatypes


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

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


# b8e4cb1b 18-Mar-2014 wenzelm <none@none>

tuned signature -- rearranged modules;


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


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

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


# 7d42ef37 23-Feb-2010 haftmann <none@none>

dropped axclass


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

removed obsolete CVS Ids;


# 803f34cc 09-Feb-2010 wenzelm <none@none>

modernized syntax translations, using mostly abbreviation/notation;
minor tuning;


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

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


# 7776a18a 16-Jun-2008 wenzelm <none@none>

sum3_instantiate: proper context;


# 04e92685 29-Mar-2008 wenzelm <none@none>

replaced 'ML_setup' by 'ML';


# 26e57f9b 30-Sep-2007 wenzelm <none@none>

avoid internal names;


# b7831de2 28-Jul-2007 wenzelm <none@none>

tuned ML/simproc declarations;


# 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


# b59abe03 01-Nov-2002 schirmer <none@none>

Inserted some extra paragraphs in large proofs to make tex run...


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


# ee7e563d 16-Jul-2002 schirmer <none@none>

Added conditional and (&&) and or (||).


# 5760fb8d 15-Jul-2002 schirmer <none@none>

fix latex output


# 560efa3a 11-Jul-2002 schirmer <none@none>

Fixed markup error in comment.


# e5e60fc1 10-Jul-2002 schirmer <none@none>

Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).


# 55bc1056 22-Feb-2002 schirmer <none@none>

Added check for field/method access to operational semantics and proved the acesses valid.


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