Session HOL-MicroJava

Theories

• HOL-Library.Transitive_Closure_Table
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• JBasis
• Type
• Decl
• TypeRel
• Value
• State
• Term
• SystemClasses
• WellForm
• WellType
• Eval
• Exceptions
• Conform
• JTypeSafe
• Example
• JListExample
• JVMState
• JVMInstructions
• JVMExecInstr
• JVMExceptions
• JVMExec
• JVMListExample
• JVMDefensive
• HOL-Library.While_Combinator
• Semilat
• Err
• Listn
• Typing_Framework
• Product
• SemilatAlg
• Typing_Framework_err
• Kildall
• Opt
• LBVSpec
• LBVCorrect
• LBVComplete
• Abstract_BV
• Semilattices
• JType
• JVMType
• Effect
• EffectMono
• BVSpec
• Typing_Framework_JVM
• LBVJVM
• Correct
• BVSpecTypeSafe
• BVNoTypeError
• JVM
• BVExample
• AuxLemmas
• DefsComp
• Index
• TranslCompTp
• TranslComp
• LemmasComp
• CorrComp
• TypeInf
• Altern
• CorrCompTp
• MicroJava