src/HOL/Bali/Eval.thy
changeset 41778 5f79a9e42507
parent 40340 d1c14898fd04
child 44890 22f665a2e91c
equal deleted inserted replaced
41777:1f7cbe39d425 41778:5f79a9e42507
    94 \item exceptions in initializations not replaced by ExceptionInInitializerError
    94 \item exceptions in initializations not replaced by ExceptionInInitializerError
    95 \end{itemize}
    95 \end{itemize}
    96 *}
    96 *}
    97 
    97 
    98 
    98 
    99 types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
    99 type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   100       vals  =        "(val, vvar, val list) sum3"
   100 type_synonym vals = "(val, vvar, val list) sum3"
   101 translations
   101 translations
   102   (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   102   (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   103   (type) "vals" <= (type) "(val, vvar, val list) sum3" 
   103   (type) "vals" <= (type) "(val, vvar, val list) sum3" 
   104 
   104 
   105 text {* To avoid redundancy and to reduce the number of rules, there is only 
   105 text {* To avoid redundancy and to reduce the number of rules, there is only