src/ZF/ex/ROOT.ML
changeset 11042 bb566dd3f927
parent 9647 e9623f47275b
child 11399 1605aeb98fd5
     1.1 --- a/src/ZF/ex/ROOT.ML	Sat Feb 03 00:11:07 2001 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Sat Feb 03 12:41:38 2001 +0100
     1.3 @@ -26,6 +26,7 @@
     1.4  time_use_thy "Rmap";            (*mapping a relation over a list*)
     1.5  time_use_thy "Mutil";           (*mutilated chess board*)
     1.6  time_use_thy "PropLog";         (*completeness of propositional logic*)
     1.7 +time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
     1.8  (*two Coq examples by Christine Paulin-Mohring*)
     1.9  time_use_thy "ListN";
    1.10  time_use_thy "Acc";