--- a/src/HOL/MicroJava/J/Example.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Thu Feb 11 00:45:02 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/MicroJava/J/Example.thy
- ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
*)
@@ -55,19 +54,16 @@
declare inj_cnam' [simp] inj_vnam' [simp]
-syntax
- Base :: cname
- Ext :: cname
- vee :: vname
- x :: vname
- e :: vname
-
-translations
- "Base" == "cnam' Base'"
- "Ext" == "cnam' Ext'"
- "vee" == "VName (vnam' vee')"
- "x" == "VName (vnam' x')"
- "e" == "VName (vnam' e')"
+abbreviation Base :: cname
+ where "Base == cnam' Base'"
+abbreviation Ext :: cname
+ where "Ext == cnam' Ext'"
+abbreviation vee :: vname
+ where "vee == VName (vnam' vee')"
+abbreviation x :: vname
+ where "x == VName (vnam' x')"
+abbreviation e :: vname
+ where "e == VName (vnam' e')"
axioms
Base_not_Object: "Base \<noteq> Object"