changeset 66453 | cc19f7ca2ed6 |
parent 63648 | f9f3006a5579 |
--- a/src/HOL/HOLCF/IOA/Seq.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/HOLCF/IOA/Seq.thy Fri Aug 18 20:47:47 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close> theory Seq -imports "../HOLCF" +imports HOLCF begin default_sort pcpo