src/HOL/NanoJava/AxSem.thy
changeset 42463 f270e3e18be5
parent 41589 bbd861837ebc
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/NanoJava/AxSem.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/NanoJava/AxSem.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -6,10 +6,10 @@
     1.4  
     1.5  theory AxSem imports State begin
     1.6  
     1.7 -types assn   = "state => bool"
     1.8 -     vassn   = "val => assn"
     1.9 -      triple = "assn \<times> stmt \<times>  assn"
    1.10 -     etriple = "assn \<times> expr \<times> vassn"
    1.11 +type_synonym assn = "state => bool"
    1.12 +type_synonym vassn = "val => assn"
    1.13 +type_synonym triple = "assn \<times> stmt \<times>  assn"
    1.14 +type_synonym etriple = "assn \<times> expr \<times> vassn"
    1.15  translations
    1.16    (type) "assn" \<leftharpoondown> (type) "state => bool"
    1.17    (type) "vassn" \<leftharpoondown> (type) "val => assn"