# HG changeset patch
# User paulson
# Date 910006514 -3600
# Node ID 9a2c90bdadfeb8c43f871e3f5abdf983bdf4f41c
# Parent  e58bb0f57c0c744b406e0d5058e943db557f642b
increased precedence of unary minus from 80 to 100

diff -r e58bb0f57c0c -r 9a2c90bdadfe src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Oct 31 12:46:21 1998 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 02 12:35:14 1998 +0100
@@ -70,7 +70,7 @@
 consts
   "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
-  uminus        :: ['a::minus] => 'a                ("- _" [80] 80)
+  uminus        :: ['a::minus] => 'a                ("- _" [100] 100)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
   (*See Nat.thy for "^"*)
 
diff -r e58bb0f57c0c -r 9a2c90bdadfe src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Sat Oct 31 12:46:21 1998 +0100
+++ b/src/HOL/ex/set.ML	Mon Nov 02 12:35:14 1998 +0100
@@ -129,7 +129,7 @@
 by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
 qed "bij_if_then_else";
 
-Goal "!!f:: 'a=>'b.  ? X. X = - (g``(- f``X))";
+Goal "? X. X = - (g``(- (f``X)))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));