--- a/src/HOL/MicroJava/J/WellType.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Sat Apr 23 13:00:19 2011 +0200
@@ -22,9 +22,8 @@
*}
text "local variables, including method parameters and This:"
-types
- lenv = "vname \<rightharpoonup> ty"
- 'c env = "'c prog \<times> lenv"
+type_synonym lenv = "vname \<rightharpoonup> ty"
+type_synonym 'c env = "'c prog \<times> lenv"
abbreviation (input)
prg :: "'c env => 'c prog"
@@ -99,7 +98,7 @@
apply auto
done
-types
+type_synonym
java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
-- "method body with parameter names, local variables, block, result expression."
-- "local variables might include This, which is hidden anyway"