New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
authorpaulson
Fri Jun 26 15:16:14 1998 +0200 (1998-06-26)
changeset 5089f95e0a6eb775
parent 5088 e4aa78d1312f
child 5090 75ac9b451ae0
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
src/HOL/Induct/LList.ML
     1.1 --- a/src/HOL/Induct/LList.ML	Fri Jun 26 15:10:40 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Fri Jun 26 15:16:14 1998 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/ex/LList
     1.5 +(*  Title:      HOL/Induct/LList
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -10,8 +10,7 @@
    1.10  
    1.11  (** Simplification **)
    1.12  
    1.13 -simpset_ref() := simpset() addsplits [split_split, split_sum_case] delsimprocs [unit_eq_proc];
    1.14 -
    1.15 +Addsplits [split_split, split_sum_case];
    1.16  
    1.17  (*This justifies using llist in other recursive type definitions*)
    1.18  Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";