diff -r cf7f3465eaf1 -r 240563fbf41d src/FOLP/ex/Foundation.thy
--- a/src/FOLP/ex/Foundation.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/FOLP/ex/Foundation.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -18,7 +18,7 @@
 apply assumption
 done
 
-text {*A form of conj-elimination*}
+text \<open>A form of conj-elimination\<close>
 schematic_lemma
   assumes "p : A & B"
     and "!!x y. x : A ==> y : B ==> f(x, y) : C"
@@ -99,7 +99,7 @@
 apply (rule refl)?
 oops
 
-text {* Parallel lifting example. *}
+text \<open>Parallel lifting example.\<close>
 schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
 apply (rule exI allI)
 apply (rule exI allI)
@@ -121,7 +121,7 @@
 apply assumption
 done
 
-text {* A bigger demonstration of quantifiers -- not in the paper. *}
+text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
 schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
 apply (rule impI)
 apply (rule allI)