| changeset 13122 | c63612ffb186 |
| parent 13114 | f2b00262bdfc |
| child 14025 | d9b155757dc8 |
--- a/src/HOL/List.ML Wed May 08 10:15:04 2002 +0200 +++ b/src/HOL/List.ML Wed May 08 12:15:30 2002 +0200 @@ -191,7 +191,6 @@ val rev_concat = thm "rev_concat"; val rev_drop = thm "rev_drop"; val rev_exhaust = thm "rev_exhaust"; -val rev_exhaust_aux = thm "rev_exhaust_aux"; val rev_induct = thm "rev_induct"; val rev_is_Nil_conv = thm "rev_is_Nil_conv"; val rev_is_rev_conv = thm "rev_is_rev_conv";