src/HOL/MicroJava/J/JBasis.thy
changeset 63258 576fb8068ba6
parent 61361 8b5f00202e1a
child 66453 cc19f7ca2ed6
equal deleted inserted replaced
63257:94d1f820130f 63258:576fb8068ba6
     4 
     4 
     5 chapter \<open>Java Source Language \label{cha:j}\<close>
     5 chapter \<open>Java Source Language \label{cha:j}\<close>
     6 
     6 
     7 section \<open>Some Auxiliary Definitions\<close>
     7 section \<open>Some Auxiliary Definitions\<close>
     8 
     8 
     9 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin 
     9 theory JBasis
       
    10 imports
       
    11   Main
       
    12   "~~/src/HOL/Library/Transitive_Closure_Table"
       
    13   "~~/src/HOL/Eisbach/Eisbach"
       
    14 begin
    10 
    15 
    11 lemmas [simp] = Let_def
    16 lemmas [simp] = Let_def
    12 
    17 
    13 subsection "unique"
    18 subsection "unique"
    14  
    19