| changeset 41144 | 509e51b7509a |
| parent 41141 | ad923cdd4a5d |
| child 42338 | 802f2fe7a0c9 |
--- a/src/HOL/Metis_Examples/ROOT.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Metis_Examples/ROOT.ML Wed Dec 15 11:26:28 2010 +0100 @@ -5,5 +5,5 @@ Testing Metis and Sledgehammer. *) -use_thys ["set", "Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski", - "TransClosure"]; +use_thys ["Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski", + "TransClosure", "set"];