author | blanchet |
Mon, 20 Jan 2014 23:43:42 +0100 | |
changeset 55090 | 9475b16e520b |
parent 55089 | 181751ad852f |
child 55091 | c43394c2e5ec |
--- a/src/HOL/Lifting_Option.thy Mon Jan 20 23:34:26 2014 +0100 +++ b/src/HOL/Lifting_Option.thy Mon Jan 20 23:43:42 2014 +0100 @@ -5,7 +5,7 @@ header {* Setup for Lifting/Transfer for the option type *} theory Lifting_Option -imports Lifting Option +imports Lifting Partial_Function begin subsection {* Relator and predicator properties *} @@ -115,4 +115,3 @@ end end -