--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu Feb 11 00:45:02 2010 +0100
@@ -296,12 +296,10 @@
done
text {* Some abbreviations for readability *}
-syntax
- Clist :: ty
- Ctest :: ty
-translations
- "Clist" == "Class list_name"
- "Ctest" == "Class test_name"
+abbreviation Clist :: ty
+ where "Clist == Class list_name"
+abbreviation Ctest :: ty
+ where "Ctest == Class test_name"
constdefs
phi_makelist :: method_type ("\<phi>\<^sub>m")