changeset 61361 | 8b5f00202e1a |
parent 58886 | 8a6cac7c7247 |
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy Wed Oct 07 23:28:49 2015 +0200 @@ -3,7 +3,7 @@ Copyright 2000 TUM *) -section {* LBV for the JVM \label{sec:JVM} *} +section \<open>LBV for the JVM \label{sec:JVM}\<close> theory LBVJVM imports Typing_Framework_JVM