changeset 27680 | 5a557a5afc48 |
parent 16417 | 9bc16273c2d4 |
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jul 25 12:03:28 2008 +0200 +++ b/src/HOL/MicroJava/BV/Typing_Framework.thy Fri Jul 25 12:03:31 2008 +0200 @@ -6,7 +6,9 @@ header {* \isaheader{Typing and Dataflow Analysis Framework} *} -theory Typing_Framework imports Listn begin +theory Typing_Framework +imports Listn +begin text {* The relationship between dataflow analysis and a welltyped-instruction predicate.