Mercurial Mercurial > hg > isabelle-cookbook / 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.
ProgTutorial/Tactical.thy
changeset 416 c6b5d1e25cdd
parent 413 95461cf6fd07
child 418 1d1e4cda8c54 
--- a/ProgTutorial/Tactical.thy	Thu Jan 14 22:10:04 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Feb 05 15:49:03 2010 +0100
@@ -2178,7 +2178,7 @@
 end"
 "Const (\"==\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
-    (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
+    (Const (\"Algebras.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
   the right-hand side should be fully beta-normalised. If instead
isabelle-cookbook