changed precedence of function update
authoroheimb
Fri Feb 18 20:24:16 2000 +0100 (2000-02-18)
changeset 8258666d3a4f3b9d
parent 8257 fe9bf28e8a58
child 8259 a8d2606f4921
changed precedence of function update
src/HOL/Fun.ML
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.ML	Fri Feb 18 18:29:28 2000 +0100
     1.2 +++ b/src/HOL/Fun.ML	Fri Feb 18 20:24:16 2000 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4  qed "fun_upd_upd";
     1.5  Addsimps [fun_upd_upd];
     1.6  
     1.7 -Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
     1.8 +Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
     1.9  by (rtac ext 1);
    1.10  by Auto_tac;
    1.11  qed "fun_upd_twist";
     2.1 --- a/src/HOL/Fun.thy	Fri Feb 18 18:29:28 2000 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Feb 18 20:24:16 2000 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4    "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
     2.5    ""               :: updbind => updbinds             ("_")
     2.6    "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
     2.7 -  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
     2.8 +  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
     2.9  
    2.10  translations
    2.11    "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"