| changeset 12911 | 704713ca07ea |
| parent 12516 | d09d0f160888 |
| child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/Kildall.thy Thu Feb 21 09:54:08 2002 +0100 @@ -6,7 +6,7 @@ Kildall's algorithm *) -header "Kildall's Algorithm" +header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *} theory Kildall = Typing_Framework + While_Combinator + Product: