# HG changeset patch
# User nipkow
# Date 1101921073 -3600
# Node ID 9234f5765d9c9b943cec476392c8404e3993ef22
# Parent  b53b89d3bf033c7d58c73158e50df94a25f281c9
Added > and >= sugar

diff -r b53b89d3bf03 -r 9234f5765d9c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Dec 01 18:10:49 2004 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 01 18:11:13 2004 +0100
@@ -343,10 +343,10 @@
 
 lemma simp_thms:
   shows not_not: "(~ ~ P) = P"
+  and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
   and
     "(P ~= Q) = (P = (~Q))"
     "(P | ~P) = True"    "(~P | P) = True"
-    "((~P) = (~Q)) = (P=Q)"
     "(x = x) = True"
     "(~True) = False"  "(~False) = True"
     "(~P) ~= P"  "P ~= (~P)"
@@ -660,9 +660,21 @@
   "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
   "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
 
+text{* Syntactic sugar: *}
 
-lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
-by blast
+consts
+  "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
+  "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
+translations
+  "x > y"  => "y < x"
+  "x >= y" => "y <= x"
+
+syntax (xsymbols)
+  "_ge"       :: "'a::ord => 'a => bool"             (infixl "\<ge>" 50)
+
+syntax (HTML output)
+  "_ge"       :: "['a::ord, 'a] => bool"             (infixl "\<ge>" 50)
+
 
 subsubsection {* Monotonicity *}
 
diff -r b53b89d3bf03 -r 9234f5765d9c src/HOL/IMPP/EvenOdd.ML
--- a/src/HOL/IMPP/EvenOdd.ML	Wed Dec 01 18:10:49 2004 +0100
+++ b/src/HOL/IMPP/EvenOdd.ML	Wed Dec 01 18:11:13 2004 +0100
@@ -77,7 +77,7 @@
 by  (force_tac Arg_Res_css 1);
 by (rtac export_s 1);
 by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
-		  ("Q1","%Z s. even Z = (s<Arg>=0)")]
+		  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
 		 (Call_invariant RS conseq12) 1);
 by (rtac (single_asm RS conseq2) 1);
 by  (clarsimp_tac Arg_Res_css 1);
diff -r b53b89d3bf03 -r 9234f5765d9c src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Wed Dec 01 18:10:49 2004 +0100
+++ b/src/HOL/IMPP/EvenOdd.thy	Wed Dec 01 18:11:13 2004 +0100
@@ -19,13 +19,13 @@
 
 constdefs
   evn :: com
- "evn == IF (%s. s<Arg>=0)
+ "evn == IF (%s. s<Arg> = 0)
          THEN Loc Res:==(%s. 0)
          ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
               Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
               Loc Res:==(%s. s<Res> * s<Arg>))"
   odd :: com
- "odd == IF (%s. s<Arg>=0)
+ "odd == IF (%s. s<Arg> = 0)
          THEN Loc Res:==(%s. 1)
          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1))"
 
@@ -37,6 +37,6 @@
  "even_Z=(Res=0)" ::        nat assn ("Res'_ok")
 defs
   Z_eq_Arg_plus_def "Z=Arg+n == %Z s.      Z =  s<Arg>+n"
-  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res>=0)"
+  Res_ok_def       "Res_ok   == %Z s. even Z = (s<Res> = 0)"
 
 end
diff -r b53b89d3bf03 -r 9234f5765d9c src/HOL/IMPP/Misc.ML
--- a/src/HOL/IMPP/Misc.ML	Wed Dec 01 18:10:49 2004 +0100
+++ b/src/HOL/IMPP/Misc.ML	Wed Dec 01 18:11:13 2004 +0100
@@ -82,8 +82,8 @@
 *)
 qed "classic_Local";
 
-Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
+Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
+\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
 by (rtac classic_Local 1);
 by (ALLGOALS Clarsimp_tac);
 by (etac conseq12 1);
@@ -92,15 +92,15 @@
 by (Asm_full_simp_tac 1);
 qed "classic_Local_indep";
 
-Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
+Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
+\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
 by (rtac export_s 1);
 by (rtac hoare_derivs.Local 1);
 by (Clarsimp_tac 1);
 qed "Local_indep";
 
-Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'>=d} |] ==> \
-\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'>=d}";
+Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
+\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
 by (rtac weak_Local 1);
 by (ALLGOALS Clarsimp_tac);
 qed "weak_Local_indep";