changeset 61361 | 8b5f00202e1a |
parent 58886 | 8a6cac7c7247 |
child 62390 | 842917225d56 |
--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Oct 07 23:28:49 2015 +0200 @@ -3,7 +3,7 @@ Copyright 1999 Technische Universitaet Muenchen *) -section {* The Lightweight Bytecode Verifier *} +section \<open>The Lightweight Bytecode Verifier\<close> theory LBVSpec imports SemilatAlg Opt