src/HOL/ex/SList.ML
changeset 2911 8a680e310f04
parent 2031 03a843f0f447
     1.1 --- a/src/HOL/ex/SList.ML	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/SList.ML	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4  local
     1.5    val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
     1.6                          Abs_list_inverse, Rep_list_inverse,
     1.7 -                        Rep_list, rangeI, inj_Leaf, Inv_f_f,
     1.8 +                        Rep_list, rangeI, inj_Leaf, inv_f_f,
     1.9                          sexp.LeafI, Rep_list_in_sexp]
    1.10  in
    1.11    val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]