src/HOL/Bali/AxSem.thy
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -58,10 +58,9 @@
     1.4    "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> CONST the_In3"
     1.5  
     1.6    --{* relation on result values, state and auxiliary variables *}
     1.7 -types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     1.8 +types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
     1.9  translations
    1.10 -      "res"    <= (type) "AxSem.res"
    1.11 -      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
    1.12 +  (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.13  
    1.14  definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
    1.15   "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"