| changeset 12036 | 49f6c49454c2 |
| parent 4098 | 71e05eb27fb6 |
| child 13454 | 01e2496dee05 |
--- a/src/HOLCF/ex/Dagstuhl.ML Sat Nov 03 18:41:13 2001 +0100 +++ b/src/HOLCF/ex/Dagstuhl.ML Sat Nov 03 18:41:28 2001 +0100 @@ -1,7 +1,5 @@ (* $Id$ *) -open Dagstuhl; - val YS_def2 = fix_prover2 Dagstuhl.thy YS_def "YS = y && YS"; val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = y && y && YYS";