src/HOL/Induct/LList.ML
changeset 5102 8c782c25a11e
parent 5089 f95e0a6eb775
child 5143 b94cd208f073
     1.1 --- a/src/HOL/Induct/LList.ML	Tue Jun 30 20:50:34 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Tue Jun 30 20:51:15 1998 +0200
     1.3 @@ -544,8 +544,8 @@
     1.4      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
     1.5  by (Fast_tac 1);
     1.6  by Safe_tac;
     1.7 -by (eres_inst_tac [("a", "u")] llist.elim 1);
     1.8 -by (eres_inst_tac [("a", "v")] llist.elim 1);
     1.9 +by (eres_inst_tac [("aa", "u")] llist.elim 1);
    1.10 +by (eres_inst_tac [("aa", "v")] llist.elim 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12  by (Blast_tac 1);
    1.13  qed "Lappend_type";
    1.14 @@ -556,7 +556,7 @@
    1.15  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
    1.16  by (etac imageI 1);
    1.17  by (rtac image_subsetI 1);
    1.18 -by (eres_inst_tac [("a", "x")] llist.elim 1);
    1.19 +by (eres_inst_tac [("aa", "x")] llist.elim 1);
    1.20  by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
    1.21  by (Asm_simp_tac 1);
    1.22  qed "Lappend_type";