| changeset 61361 | 8b5f00202e1a |
| parent 35416 | d8d7d1b785af |
| child 62390 | 842917225d56 |
--- a/src/HOL/MicroJava/J/Exceptions.thy Wed Oct 07 19:45:00 2015 +0200 +++ b/src/HOL/MicroJava/J/Exceptions.thy Wed Oct 07 23:28:49 2015 +0200 @@ -5,7 +5,7 @@ theory Exceptions imports State begin -text {* a new, blank object with default values in all fields: *} +text \<open>a new, blank object with default values in all fields:\<close> definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where "blank G C \<equiv> (C,init_vars (fields(G,C)))"