merged
authornipkow
Thu Oct 20 10:44:00 2011 +0200 (2011-10-20)
changeset 45217c4fab1099cd0
parent 45215 1b2132017774
parent 45216 a51a70687517
child 45218 f115540543d8
child 45219 29f6e990674d
child 45222 6eab55bab82f
merged
     1.1 --- a/src/HOL/IMP/AExp.thy	Thu Oct 20 09:59:12 2011 +0200
     1.2 +++ b/src/HOL/IMP/AExp.thy	Thu Oct 20 10:44:00 2011 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  datatype aexp = N int | V vname | Plus aexp aexp
     1.5  
     1.6  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
     1.7 -"aval (N n) _ = n" |
     1.8 +"aval (N n) s = n" |
     1.9  "aval (V x) s = s x" |
    1.10  "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
    1.11  
     2.1 --- a/src/HOL/IMP/BExp.thy	Thu Oct 20 09:59:12 2011 +0200
     2.2 +++ b/src/HOL/IMP/BExp.thy	Thu Oct 20 10:44:00 2011 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
     2.5  
     2.6  fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
     2.7 -"bval (Bc v) _ = v" |
     2.8 +"bval (Bc v) s = v" |
     2.9  "bval (Not b) s = (\<not> bval b s)" |
    2.10  "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
    2.11  "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"