--- a/src/HOL/NanoJava/Example.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/NanoJava/Example.thy Thu May 26 17:51:22 2016 +0200
@@ -9,7 +9,7 @@
imports Equivalence
begin
-text {*
+text \<open>
\begin{verbatim}
class Nat {
@@ -39,7 +39,7 @@
}
\end{verbatim}
-*}
+\<close>
axiomatization where
This_neq_Par [simp]: "This \<noteq> Par" and
@@ -62,8 +62,8 @@
one :: expr
where "one == {Nat}new Nat..suc(<>)"
-text {* The following properties could be derived from a more complete
- program model, which we leave out for laziness. *}
+text \<open>The following properties could be derived from a more complete
+ program model, which we leave out for laziness.\<close>
axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"