changeset 61361 | 8b5f00202e1a |
parent 58886 | 8a6cac7c7247 |
child 61994 | 133a8a888ae8 |
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Wed Oct 07 23:28:49 2015 +0200 @@ -3,7 +3,7 @@ Copyright 2000 Technische Universitaet Muenchen *) -section {* Completeness of the LBV *} +section \<open>Completeness of the LBV\<close> theory LBVComplete imports LBVSpec Typing_Framework