Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Update.ML
changeset 9907 473a6604da94
parent 6068 2d8f3e1f1151 
--- a/src/ZF/Update.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/Update.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      ZF/Update.thy
+(*  Title:      ZF/Update.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -6,8 +6,6 @@
 Function updates: like theory Map, but for ordinary functions
 *)
 
-open Update;
-
 Goal "f(x:=y) ` z = (if z=x then y else f`z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 by (case_tac "z : domain(f)" 1);
isabelle