author | paulson |
Mon, 28 Dec 1998 16:53:24 +0100 | |
changeset 6045 | 6a9dc67d48f5 |
parent 6044 | e0f9d930e956 |
child 6046 | 2c8a8be36c94 |
src/ZF/ex/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/ZF/ex/ROOT.ML Mon Dec 28 16:52:51 1998 +0100 +++ b/src/ZF/ex/ROOT.ML Mon Dec 28 16:53:24 1998 +0100 @@ -28,7 +28,7 @@ (** Inductive definitions **) time_use_thy "Rmap"; (*mapping a relation over a list*) -time_use_thy "Mutil"; (*mutilated checkerboard*) +time_use_thy "Mutil"; (*mutilated chess board*) time_use_thy "PropLog"; (*completeness of propositional logic*) (*two Coq examples by Christine Paulin-Mohring*) time_use_thy "ListN";