History log of /seL4-l4v-10.1.1/isabelle/src/HOL/MicroJava/JVM/JVMExecInstr.thy
Revision Date Author Comments
# 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;


# ba266305 07-Oct-2015 wenzelm <none@none>

isabelle update_cartouches;


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

modernized header;


# 870b0a5d 27-Sep-2010 haftmann <none@none>

modernized primrecs


# c040dd23 24-Nov-2009 haftmann <none@none>

backported parts of abstract byte code verifier from AFP/Jinja

--HG--
extra : rebase_source : 1d943bc92831d0a92004a43f72ff37eb352bf23f


# 16362266 07-Oct-2008 haftmann <none@none>

arbitrary is undefined


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

migrated theory headers to new format


# 89a6f329 23-Oct-2002 kleing <none@none>

cleanup, beautified


# 0e7365d8 21-Feb-2002 kleing <none@none>

new document


# 09f51db6 15-Dec-2001 kleing <none@none>

exception merge + cleanup


# a8eb3930 16-Jan-2001 kleing <none@none>

newref -> new_Addr


# ef8f4a2b 14-Jan-2001 kleing <none@none>

removed instructions Aconst_null+Bipush, introduced LitPush


# c9fd864f 05-Dec-2000 kleing <none@none>

jvm_progs now also store maximum op_stack depth


# 339494fb 22-Sep-2000 kleing <none@none>

converted to Isar, tuned


# ddf2a7ee 21-Sep-2000 kleing <none@none>

tuned spacing for document generation


# 3d045495 21-Sep-2000 kleing <none@none>

unsymbolized


# 53b728cd 07-Aug-2000 kleing <none@none>

Invoke instruction gets fully qualified method name (class+name+sig) as
in Sun's JVM spec


# ab66f32d 17-Jul-2000 kleing <none@none>

flat instruction set