increased precedence of unary minus from 80 to 100
authorpaulson
Mon Nov 02 12:35:14 1998 +0100 (1998-11-02)
changeset 57869a2c90bdadfe
parent 5785 e58bb0f57c0c
child 5787 4e5c74b7cd9e
increased precedence of unary minus from 80 to 100
src/HOL/HOL.thy
src/HOL/ex/set.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Oct 31 12:46:21 1998 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 02 12:35:14 1998 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  consts
     1.5    "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
     1.6    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
     1.7 -  uminus        :: ['a::minus] => 'a                ("- _" [80] 80)
     1.8 +  uminus        :: ['a::minus] => 'a                ("- _" [100] 100)
     1.9    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.10    (*See Nat.thy for "^"*)
    1.11  
     2.1 --- a/src/HOL/ex/set.ML	Sat Oct 31 12:46:21 1998 +0100
     2.2 +++ b/src/HOL/ex/set.ML	Mon Nov 02 12:35:14 1998 +0100
     2.3 @@ -129,7 +129,7 @@
     2.4  by (fast_tac (claset() addEs  [inj_onD, f_eq_gE]) 1);
     2.5  qed "bij_if_then_else";
     2.6  
     2.7 -Goal "!!f:: 'a=>'b.  ? X. X = - (g``(- f``X))";
     2.8 +Goal "? X. X = - (g``(- (f``X)))";
     2.9  by (rtac exI 1);
    2.10  by (rtac lfp_Tarski 1);
    2.11  by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));