changeset 5717 | 0d28dbe484b6 |
parent 5191 | 8ceaa19f7717 |
child 5738 | 0d8698c15439 |
--- a/src/HOL/Induct/Term.thy Wed Oct 21 17:46:00 1998 +0200 +++ b/src/HOL/Induct/Term.thy Wed Oct 21 17:48:02 1998 +0200 @@ -28,7 +28,7 @@ inductive "term(A)" intrs APP_I "[| M: A; N : list(term(A)) |] ==> Scons M N : term(A)" - monos "[list_mono]" + monos list_mono defs (*defining abstraction/representation functions for term list...*)