| changeset 42343 | 118cc349de35 |
| parent 42338 | 802f2fe7a0c9 |
| child 43162 | 9a8acc5adfa3 |
--- a/src/HOL/Metis_Examples/ROOT.ML Thu Apr 14 11:24:05 2011 +0200 +++ b/src/HOL/Metis_Examples/ROOT.ML Thu Apr 14 11:24:05 2011 +0200 @@ -5,5 +5,5 @@ Testing Metis and Sledgehammer. *) -use_thys ["Abstraction", "BigO", "BT", "Clausifier", "HO_Reas", "Message", +use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message", "Tarski", "TransClosure", "set"];