src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
changeset 61424 c3658c18b7bc
parent 61032 b57df8eecad6
child 62000 8cba509ace9c
     1.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4  fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
     1.5                                THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
     1.6  
     1.7 -fun pair_tac s = rule_tac p",s)] PairE
     1.8 +fun pair_tac s = rule_tac p",s)] prod.exhaust
     1.9                            THEN' hyp_subst_tac THEN' Simp_tac;
    1.10  *)
    1.11  (* induction on a sequence of pairs with pairsplitting and simplification *)
    1.12 @@ -1102,7 +1102,7 @@
    1.13    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
    1.14  
    1.15  fun pair_tac ctxt s =
    1.16 -  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
    1.17 +  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm prod.exhaust}
    1.18    THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
    1.19  
    1.20  (* induction on a sequence of pairs with pairsplitting and simplification *)