changeset 11481 | c77e5401f2ff |
parent 8840 | 18b76c137c41 |
--- a/src/HOL/Induct/Sexp.ML Wed Aug 08 14:50:28 2001 +0200 +++ b/src/HOL/Induct/Sexp.ML Wed Aug 08 14:51:10 2001 +0200 @@ -6,8 +6,6 @@ S-expressions, general binary trees for defining recursive data structures *) -open Sexp; - (** sexp_case **) Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";