doc-src/IsarRef/Thy/Spec.thy
changeset 40800 330eb65c9469
parent 40784 177e8cea3e09
child 41249 26f12f98f50a
--- a/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 20:36:45 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Sun Nov 28 21:07:28 2010 +0100
@@ -1164,7 +1164,7 @@
 
   \end{description}
 
-  See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
+  See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
   defining a new primitive rule as oracle, and turning it into a proof
   method.
 *}