23449
|
1 |
(* Title: HOL/MetisExamples/ROOT.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
|
25709
|
5 |
Testing the metis method.
|
23449
|
6 |
*)
|
|
7 |
|
25709
|
8 |
use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];
|
|
9 |
|