src/HOL/MicroJava/BV/DFA_Framework.thy

--- a/src/HOL/MicroJava/BV/DFA_Framework.thy	Fri Feb 09 11:40:10 2001 +0100
+++ b/src/HOL/MicroJava/BV/DFA_Framework.thy	Fri Feb 09 16:01:58 2001 +0100
@@ -2,14 +2,16 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TUM
-
-The relationship between dataflow analysis and a welltyped-insruction predicate.
 *)
 
 header "Dataflow Analysis Framework"
 
 theory DFA_Framework = Listn:
 
+text {* 
+  The relationship between dataflow analysis and a welltyped-insruction predicate. 
+*}
+
 constdefs
  bounded :: "(nat => nat list) => nat => bool"
 "bounded succs n == !p<n. !q:set(succs p). q<n"