src/HOL/MicroJava/BV/Typing_Framework.thy
changeset 16417 9bc16273c2d4
parent 14653 0848ab6fe5fc
child 27680 5a557a5afc48
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     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 = Listn:
     9 theory Typing_Framework imports Listn begin
    10 
    10 
    11 text {* 
    11 text {* 
    12   The relationship between dataflow analysis and a welltyped-instruction predicate. 
    12   The relationship between dataflow analysis and a welltyped-instruction predicate. 
    13 *}
    13 *}
    14 types
    14 types