diff -r 9de1eb745aeb -r 5d208fd2507d src/FOLP/ex/Intro.thy
--- a/src/FOLP/ex/Intro.thy	Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOLP/ex/Intro.thy	Fri Jan 01 10:49:00 2016 +0100
@@ -41,7 +41,7 @@
 done
 
 
-subsubsection \<open>Demonstration of @{text "fast"}\<close>
+subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
 
 schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
         -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"