src/ZF/ex/ROOT.ML
changeset 1613 44f5255cba9e
parent 1461 6bcb44e4d6e5
child 1793 09fff2f0d727
--- a/src/ZF/ex/ROOT.ML	Tue Mar 26 11:58:59 1996 +0100
+++ b/src/ZF/ex/ROOT.ML	Tue Mar 26 12:01:13 1996 +0100
@@ -29,6 +29,7 @@
 
 (** Inductive definitions **)
 time_use_thy "Rmap";            (*mapping a relation over a list*)
+time_use_thy "Mutil";           (*mutilated checkerboard*)
 time_use_thy "PropLog";         (*completeness of propositional logic*)
 (*two Coq examples by Christine Paulin-Mohring*)
 time_use_thy "ListN";