src/HOL/ex/LList.ML
changeset 2911 8a680e310f04
parent 2596 3b4ad6c7726f
child 2950 5d2e0865ecf3
     1.1 --- a/src/HOL/ex/LList.ML	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/LList.ML	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -557,7 +557,7 @@
     1.4  (** llist_case: case analysis for 'a llist **)
     1.5  
     1.6  Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
     1.7 -           Rep_llist, rangeI, inj_Leaf, Inv_f_f] @ llist.intrs);
     1.8 +           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
     1.9  
    1.10  goalw LList.thy [llist_case_def,LNil_def]  "llist_case c d LNil = c";
    1.11  by (Simp_tac 1);