Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed precedence of function update
authoroheimb
Fri, 18 Feb 2000 20:24:16 +0100
changeset 8258 666d3a4f3b9d
parent 8257 fe9bf28e8a58
child 8259 a8d2606f4921
changed precedence of function update
src/HOL/Fun.ML file | annotate | diff | comparison | revisions
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.ML	Fri Feb 18 18:29:28 2000 +0100
+++ b/src/HOL/Fun.ML	Fri Feb 18 20:24:16 2000 +0100
@@ -420,7 +420,7 @@
 qed "fun_upd_upd";
 Addsimps [fun_upd_upd];
 
-Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
+Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
 by (rtac ext 1);
 by Auto_tac;
 qed "fun_upd_twist";
--- a/src/HOL/Fun.thy	Fri Feb 18 18:29:28 2000 +0100
+++ b/src/HOL/Fun.thy	Fri Feb 18 20:24:16 2000 +0100
@@ -23,7 +23,7 @@
   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
   ""               :: updbind => updbinds             ("_")
   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
-  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
+  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
 
 translations
   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
isabelle