--- a/src/HOL/IMP/Vars.thy Thu Nov 22 22:21:54 2012 +0100
+++ b/src/HOL/IMP/Vars.thy Fri Nov 23 13:46:01 2012 +0100
@@ -31,7 +31,7 @@
end
-value "vars(Plus (V ''x'') (V ''y''))"
+value "vars (Plus (V ''x'') (V ''y''))"
instantiation bexp :: vars
begin
@@ -46,7 +46,7 @@
end
-value "show (vars(Less (Plus (V ''z'') (V ''y'')) (V ''x'')))"
+value "vars (Less (Plus (V ''z'') (V ''y'')) (V ''x''))"
abbreviation
eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"