--- a/src/HOL/NanoJava/AxSem.thy Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Sat Apr 23 13:00:19 2011 +0200
@@ -6,10 +6,10 @@
theory AxSem imports State begin
-types assn = "state => bool"
- vassn = "val => assn"
- triple = "assn \<times> stmt \<times> assn"
- etriple = "assn \<times> expr \<times> vassn"
+type_synonym assn = "state => bool"
+type_synonym vassn = "val => assn"
+type_synonym triple = "assn \<times> stmt \<times> assn"
+type_synonym etriple = "assn \<times> expr \<times> vassn"
translations
(type) "assn" \<leftharpoondown> (type) "state => bool"
(type) "vassn" \<leftharpoondown> (type) "val => assn"