src/HOL/Datatype.ML
changeset 9108 9fff97d29837
parent 7293 959e060f4a2f
child 11954 3d1780208bf3
equal deleted inserted replaced
9107:67202a50ee6d 9108:9fff97d29837
     6 
     6 
     7 (** sum_case -- the selection operator for sums **)
     7 (** sum_case -- the selection operator for sums **)
     8 
     8 
     9 (*compatibility*)
     9 (*compatibility*)
    10 val [sum_case_Inl, sum_case_Inr] = sum.cases;
    10 val [sum_case_Inl, sum_case_Inr] = sum.cases;
       
    11 bind_thm ("sum_case_Inl", sum_case_Inl);
       
    12 bind_thm ("sum_case_Inr", sum_case_Inr);
    11 
    13 
    12 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    14 Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
    13 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    15 by (EVERY1 [res_inst_tac [("s","s")] sumE, 
    14             etac ssubst, rtac sum_case_Inl,
    16             etac ssubst, rtac sum_case_Inl,
    15             etac ssubst, rtac sum_case_Inr]);
    17             etac ssubst, rtac sum_case_Inr]);