diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Thu May 26 17:51:22 2016 +0200
@@ -7,24 +7,24 @@
 imports "../../SPARK"
 begin
 
-text {*
+text \<open>
 Set of all increasing subsequences in a prefix of an array
-*}
+\<close>
 
 definition iseq :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat set set" where
   "iseq xs l = {is. (\<forall>i\<in>is. i < l) \<and>
      (\<forall>i\<in>is. \<forall>j\<in>is. i \<le> j \<longrightarrow> xs i \<le> xs j)}"
 
-text {*
+text \<open>
 Length of longest increasing subsequence in a prefix of an array
-*}
+\<close>
 
 definition liseq :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat" where
   "liseq xs i = Max (card ` iseq xs i)"
 
-text {*
+text \<open>
 Length of longest increasing subsequence ending at a particular position
-*}
+\<close>
 
 definition liseq' :: "(nat \<Rightarrow> 'a::linorder) \<Rightarrow> nat \<Rightarrow> nat" where
   "liseq' xs i = Max (card ` (iseq xs (Suc i) \<inter> {is. Max is = i}))"
@@ -238,8 +238,8 @@
           by (simp add: card_insert max_notin)
         moreover {
           from H j have "xs (Max is) \<le> xs i" by simp
-          moreover from `j < i` have "Suc j \<le> i" by simp
-          with `is \<in> iseq xs (Suc j)` have "is \<in> iseq xs i"
+          moreover from \<open>j < i\<close> have "Suc j \<le> i" by simp
+          with \<open>is \<in> iseq xs (Suc j)\<close> have "is \<in> iseq xs i"
             by (rule iseq_mono)
           ultimately have "is \<union> {i} \<in> iseq xs (Suc i)"
           by (rule iseq_insert)
@@ -269,52 +269,52 @@
         then have "1 < card is" by simp
         then have "Max (is - {Max is}) < Max is"
           by (rule Max_diff)
-        from `is \<in> iseq xs (Suc i)` `1 < card is`
+        from \<open>is \<in> iseq xs (Suc i)\<close> \<open>1 < card is\<close>
         have "xs (Max (is - {Max is})) \<le> xs (Max is)"
           by (rule iseq_nth)
         have "card is - 1 = liseq' xs (Max (is - {i}))"
         proof (rule liseq'_eq)
-          from `Max is = i` [symmetric] `finite is` `is \<noteq> {}`
+          from \<open>Max is = i\<close> [symmetric] \<open>finite is\<close> \<open>is \<noteq> {}\<close>
           show "card is - 1 = card (is - {i})" by simp
         next
-          from `is \<in> iseq xs (Suc i)` `Max is = i` [symmetric]
+          from \<open>is \<in> iseq xs (Suc i)\<close> \<open>Max is = i\<close> [symmetric]
           show "is - {i} \<in> iseq xs (Suc (Max (is - {i})))"
             by simp (rule iseq_diff)
         next
-          from `1 < card is`
+          from \<open>1 < card is\<close>
           show "is - {i} \<noteq> {}" by (rule diff_nonempty)
         next
           fix js
           assume "js \<in> iseq xs (Suc (Max (is - {i})))"
             "Max js = Max (is - {i})" "finite js" "js \<noteq> {}"
-          from `xs (Max (is - {Max is})) \<le> xs (Max is)`
-            `Max js = Max (is - {i})` `Max is = i`
+          from \<open>xs (Max (is - {Max is})) \<le> xs (Max is)\<close>
+            \<open>Max js = Max (is - {i})\<close> \<open>Max is = i\<close>
           have "xs (Max js) \<le> xs i" by simp
-          moreover from `Max is = i` `Max (is - {Max is}) < Max is`
+          moreover from \<open>Max is = i\<close> \<open>Max (is - {Max is}) < Max is\<close>
           have "Suc (Max (is - {i})) \<le> i"
             by simp
-          with `js \<in> iseq xs (Suc (Max (is - {i})))`
+          with \<open>js \<in> iseq xs (Suc (Max (is - {i})))\<close>
           have "js \<in> iseq xs i"
             by (rule iseq_mono)
           ultimately have "js \<union> {i} \<in> iseq xs (Suc i)"
             by (rule iseq_insert)
-          moreover from `js \<noteq> {}` `finite js` `Max js = Max (is - {i})`
-            `Max is = i` [symmetric] `Max (is - {Max is}) < Max is`
+          moreover from \<open>js \<noteq> {}\<close> \<open>finite js\<close> \<open>Max js = Max (is - {i})\<close>
+            \<open>Max is = i\<close> [symmetric] \<open>Max (is - {Max is}) < Max is\<close>
           have "Max (js \<union> {i}) = i"
             by simp
           ultimately have "card (js \<union> {i}) \<le> card is" by (rule R)
-          moreover from `Max is = i` [symmetric] `finite js`
-            `Max (is - {Max is}) < Max is` `Max js = Max (is - {i})`
+          moreover from \<open>Max is = i\<close> [symmetric] \<open>finite js\<close>
+            \<open>Max (is - {Max is}) < Max is\<close> \<open>Max js = Max (is - {i})\<close>
           have "i \<notin> js" by (simp add: max_notin)
-          with `finite js`
+          with \<open>finite js\<close>
           have "card (js \<union> {i}) = card ((js \<union> {i}) - {i}) + 1"
             by simp
           ultimately show "card js \<le> card (is - {i})"
-            using `i \<notin> js` `Max is = i` [symmetric] `is \<noteq> {}` `finite is`
+            using \<open>i \<notin> js\<close> \<open>Max is = i\<close> [symmetric] \<open>is \<noteq> {}\<close> \<open>finite is\<close>
             by simp
         qed simp
-        with H `Max (is - {Max is}) < Max is`
-          `xs (Max (is - {Max is})) \<le> xs (Max is)`
+        with H \<open>Max (is - {Max is}) < Max is\<close>
+          \<open>xs (Max (is - {Max is})) \<le> xs (Max is)\<close>
         show ?thesis by auto
       qed
     qed
@@ -515,7 +515,7 @@
   done
 
 
-text {* Proof functions *}
+text \<open>Proof functions\<close>
 
 abbreviation (input)
   "arr_conv a \<equiv> (\<lambda>n. a (int n))"
@@ -539,7 +539,7 @@
   max_ext = "max_ext' :: (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int"
 
 
-text {* The verification conditions *}
+text \<open>The verification conditions\<close>
 
 spark_open "liseq/liseq_length"