| changeset 61361 | 8b5f00202e1a |
| parent 58886 | 8a6cac7c7247 |
| child 62042 | 6c6ccf573479 |
--- a/src/HOL/MicroJava/DFA/Kildall.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Wed Oct 07 23:28:49 2015 +0200 @@ -3,7 +3,7 @@ Copyright 2000 TUM *) -section {* Kildall's Algorithm \label{sec:Kildall} *} +section \<open>Kildall's Algorithm \label{sec:Kildall}\<close> theory Kildall imports SemilatAlg "~~/src/HOL/Library/While_Combinator"