# HG changeset patch
# User nipkow
# Date 1367202042 -7200
# Node ID 1006b9b08d7394d6f720d2e37402a964bf0fa972
# Parent  674522b0d06d4fca62de4597b99d0d95c42f15f5
tuned

diff -r 674522b0d06d -r 1006b9b08d73 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Apr 28 09:10:43 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Apr 29 04:20:42 2013 +0200
@@ -9,29 +9,26 @@
 datatype const = Const val | Any
 
 fun \<gamma>_const where
-"\<gamma>_const (Const n) = {n}" |
+"\<gamma>_const (Const i) = {i}" |
 "\<gamma>_const (Any) = UNIV"
 
 fun plus_const where
-"plus_const (Const m) (Const n) = Const(m+n)" |
+"plus_const (Const i) (Const j) = Const(i+j)" |
 "plus_const _ _ = Any"
 
 lemma plus_const_cases: "plus_const a1 a2 =
-  (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
+  (case (a1,a2) of (Const i, Const j) \<Rightarrow> Const(i+j) | _ \<Rightarrow> Any)"
 by(auto split: prod.split const.split)
 
 instantiation const :: semilattice
 begin
 
-fun less_eq_const where
-"_ \<le> Any = True" |
-"Const n \<le> Const m = (n=m)" |
-"Any \<le> Const _ = False"
+fun less_eq_const where "x \<le> y = (y = Any | x=y)"
 
-definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
+definition "x < (y::const) = (x \<le> y & \<not> y \<le> x)"
 
 fun sup_const where
-"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
+"Const i \<squnion> Const j = (if i=j then Const i else Any)" |
 "_ \<squnion> _ = Any"
 
 definition "\<top> = Any"