| changeset 5717 | 0d28dbe484b6 |
| parent 5184 | 9b8547a9496a |
| child 6481 | dbf2d9b3d6c8 |
--- a/src/HOL/ex/Primrec.thy Wed Oct 21 17:46:00 1998 +0200 +++ b/src/HOL/ex/Primrec.thy Wed Oct 21 17:48:02 1998 +0200 @@ -67,6 +67,6 @@ PROJ "PROJ i : PRIMREC" COMP "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC" PREC "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC" - monos "[lists_mono]" + monos lists_mono end