--- a/src/HOL/MicroJava/J/WellForm.thy Wed Oct 07 19:45:00 2015 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Wed Oct 07 23:28:49 2015 +0200
@@ -3,13 +3,13 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-section {* Well-formedness of Java programs *}
+section \<open>Well-formedness of Java programs\<close>
theory WellForm
imports TypeRel SystemClasses
begin
-text {*
+text \<open>
for static checks on expressions and statements, see WellType.
\begin{description}
@@ -24,7 +24,7 @@
\item for uniformity, Object is assumed to be declared like any other class
\end{itemize}
\end{description}
-*}
+\<close>
type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
definition wf_syscls :: "'c prog => bool" where