Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/BVExample.thy
changeset 24351 1e028d114075
parent 24340 811f78424efc
child 28520 376b9c083b04
equal deleted inserted replaced
24350:4d74f37c6367 24351:1e028d114075 
     4 *)
 
     4 *)
 
     5 
     5 
     6 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
     6 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
     7 
     7 
     8 theory BVExample
 
     8 theory BVExample
 
     9 imports "../JVM/JVMListExample" BVSpecTypeSafe "../JVM/JVM" Executable_Set
 
     9 imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set
 
    10 begin
 
    10 begin
 
    11 
    11 
    12 text {*
 
    12 text {*
 
    13   This theory shows type correctness of the example program in section 
    13   This theory shows type correctness of the example program in section 
    14   \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
 
    14   \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
isabelle