src/HOL/Library/Quotient_Option.thy
changeset 58916 229765cc3414
parent 58881 b9556a055632
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Nov 07 12:24:56 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Nov 07 11:28:37 2014 +0100
     1.3 @@ -54,12 +54,12 @@
     1.4  lemma option_None_rsp [quot_respect]:
     1.5    assumes q: "Quotient3 R Abs Rep"
     1.6    shows "rel_option R None None"
     1.7 -  by (rule None_transfer)
     1.8 +  by (rule option.ctr_transfer(1))
     1.9  
    1.10  lemma option_Some_rsp [quot_respect]:
    1.11    assumes q: "Quotient3 R Abs Rep"
    1.12    shows "(R ===> rel_option R) Some Some"
    1.13 -  by (rule Some_transfer)
    1.14 +  by (rule option.ctr_transfer(2))
    1.15  
    1.16  lemma option_None_prs [quot_preserve]:
    1.17    assumes q: "Quotient3 R Abs Rep"