src/HOL/List.ML
changeset 6141 a6922171b396
parent 6073 fba734ba6894
child 6162 484adda70b65
equal deleted inserted replaced
6140:af32e2c3f77a 6141:a6922171b396
    30 Goalw lists.defs "A<=B ==> lists A <= lists B";
    30 Goalw lists.defs "A<=B ==> lists A <= lists B";
    31 by (rtac lfp_mono 1);
    31 by (rtac lfp_mono 1);
    32 by (REPEAT (ares_tac basic_monos 1));
    32 by (REPEAT (ares_tac basic_monos 1));
    33 qed "lists_mono";
    33 qed "lists_mono";
    34 
    34 
    35 val listsE = lists.mk_cases list.simps  "x#l : lists A";
    35 val listsE = lists.mk_cases "x#l : lists A";
    36 AddSEs [listsE];
    36 AddSEs [listsE];
    37 AddSIs lists.intrs;
    37 AddSIs lists.intrs;
    38 
    38 
    39 Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
    39 Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
    40 by (etac lists.induct 1);
    40 by (etac lists.induct 1);