src/HOL/MicroJava/BV/Typing_Framework.thy
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.