delsimprocs [unit_eq_proc];
authorwenzelm
Thu Jun 25 16:13:20 1998 +0200 (1998-06-25)
changeset 5086ef479934678b
parent 5085 8e5a7942fdea
child 5087 ee8a754f1981
delsimprocs [unit_eq_proc];
src/HOL/Induct/LList.ML
     1.1 --- a/src/HOL/Induct/LList.ML	Thu Jun 25 16:12:02 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Thu Jun 25 16:13:20 1998 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (** Simplification **)
     1.6  
     1.7 -simpset_ref() := simpset() addsplits [split_split, split_sum_case];
     1.8 +simpset_ref() := simpset() addsplits [split_split, split_sum_case] delsimprocs [unit_eq_proc];
     1.9  
    1.10  
    1.11  (*This justifies using llist in other recursive type definitions*)