author | blanchet |
Thu, 14 Apr 2011 11:24:05 +0200 | |
changeset 42343 | 118cc349de35 |
parent 42338 | 802f2fe7a0c9 |
child 43162 | 9a8acc5adfa3 |
permissions | -rw-r--r-- |
33027 | 1 |
(* Title: HOL/Metis_Examples/ROOT.ML |
23449 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
41141
ad923cdd4a5d
added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
33027
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
23449 | 4 |
|
41141
ad923cdd4a5d
added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
33027
diff
changeset
|
5 |
Testing Metis and Sledgehammer. |
23449 | 6 |
*) |
7 |
||
42343 | 8 |
use_thys ["Abstraction", "BigO", "BT", "Clausify", "HO_Reas", "Message", |
42338 | 9 |
"Tarski", "TransClosure", "set"]; |