changeset 2911 | 8a680e310f04 |
parent 1476 | 608483c2122a |
--- a/src/HOL/ex/Term.thy Fri Apr 04 16:16:35 1997 +0200 +++ b/src/HOL/ex/Term.thy Fri Apr 04 16:27:39 1997 +0200 @@ -45,7 +45,7 @@ term_rec_def "term_rec t d == - Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)" + Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)" rules (*faking a type definition for term...*)