| changeset 5717 | 0d28dbe484b6 |
| parent 5261 | ce3c25c8a694 |
| child 9102 | c7ba07e3bbe8 |
--- a/src/HOL/Lambda/InductTermi.thy Wed Oct 21 17:46:00 1998 +0200 +++ b/src/HOL/Lambda/InductTermi.thy Wed Oct 21 17:48:02 1998 +0200 @@ -17,6 +17,6 @@ VarI "rs : lists IT ==> (Var n)$$rs : IT" LambdaI "r : IT ==> Abs r : IT" BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" -monos "[lists_mono]" +monos lists_mono end