| changeset 66992 | 69673025292e |
| parent 66453 | cc19f7ca2ed6 |
| child 69605 | a96320074298 |
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Thu Nov 02 15:21:35 2017 +0100 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Fri Nov 03 13:43:31 2017 +0100 @@ -4,7 +4,7 @@ *) theory Longest_Increasing_Subsequence -imports SPARK +imports "HOL-SPARK.SPARK" begin text \<open>