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/HOL/Modelcheck/MuckeSyn.thy
changeset 26957 e3f04fdd994d
parent 26939 1035c89b4c02
child 28263 69eaa97e7e96 
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:20 2008 +0200
@@ -164,7 +164,7 @@
 
 (* transforming fun-defs into lambda-defs *)
 
-val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
+val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
  by (rtac (extensional eq) 1);
 qed "ext_rl";
isabelle