equal
deleted
inserted
replaced
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *} |
7 header {* \isaheader{The Typing Framework for the JVM}\label{sec:JVM} *} |
8 |
8 |
9 theory Typing_Framework_JVM = Typing_Framework_err + JVMType + EffectMono + BVSpec: |
9 theory Typing_Framework_JVM imports Typing_Framework_err JVMType EffectMono BVSpec begin |
10 |
10 |
11 |
11 |
12 constdefs |
12 constdefs |
13 exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type" |
13 exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type" |
14 "exec G maxs rT et bs == |
14 "exec G maxs rT et bs == |