src/HOL/MicroJava/BV/Typing_Framework.thy
changeset 27680 5a557a5afc48
parent 16417 9bc16273c2d4
equal deleted inserted replaced
27679:6392b92c3536 27680:5a557a5afc48
     4     Copyright   2000 TUM
     4     Copyright   2000 TUM
     5 *)
     5 *)
     6 
     6 
     7 header {* \isaheader{Typing and Dataflow Analysis Framework} *}
     7 header {* \isaheader{Typing and Dataflow Analysis Framework} *}
     8 
     8 
     9 theory Typing_Framework imports Listn begin
     9 theory Typing_Framework
       
    10 imports Listn
       
    11 begin
    10 
    12 
    11 text {* 
    13 text {* 
    12   The relationship between dataflow analysis and a welltyped-instruction predicate. 
    14   The relationship between dataflow analysis and a welltyped-instruction predicate. 
    13 *}
    15 *}
    14 types
    16 types