src/HOL/List.ML
changeset 6141 a6922171b396
parent 6073 fba734ba6894
child 6162 484adda70b65
     1.1 --- a/src/HOL/List.ML	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  by (REPEAT (ares_tac basic_monos 1));
     1.5  qed "lists_mono";
     1.6  
     1.7 -val listsE = lists.mk_cases list.simps  "x#l : lists A";
     1.8 +val listsE = lists.mk_cases "x#l : lists A";
     1.9  AddSEs [listsE];
    1.10  AddSIs lists.intrs;
    1.11