technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
authorblanchet
Mon Jan 20 23:43:42 2014 +0100 (2014-01-20)
changeset 550909475b16e520b
parent 55089 181751ad852f
child 55091 c43394c2e5ec
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
src/HOL/Lifting_Option.thy
     1.1 --- a/src/HOL/Lifting_Option.thy	Mon Jan 20 23:34:26 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Mon Jan 20 23:43:42 2014 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Setup for Lifting/Transfer for the option type *}
     1.5  
     1.6  theory Lifting_Option
     1.7 -imports Lifting Option
     1.8 +imports Lifting Partial_Function
     1.9  begin
    1.10  
    1.11  subsection {* Relator and predicator properties *}
    1.12 @@ -115,4 +115,3 @@
    1.13  end
    1.14  
    1.15  end
    1.16 -