src/HOL/Metis_Examples/ROOT.ML
author huffman
Thu, 29 Apr 2010 09:17:25 -0700
changeset 36591 df38e0c5c123
parent 33027 9cf389429f6d
child 41141 ad923cdd4a5d
permissions -rw-r--r--
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy

(*  Title:      HOL/Metis_Examples/ROOT.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Testing the metis method.
*)

use_thys ["set", "BigO", "Abstraction", "BT", "Message", "Tarski", "TransClosure"];