src/HOL/Metis_Examples/ROOT.ML
author blanchet
Wed Dec 15 11:26:28 2010 +0100 (2010-12-15)
changeset 41141 ad923cdd4a5d
parent 33027 9cf389429f6d
child 41144 509e51b7509a
permissions -rw-r--r--
added example to exercise higher-order reasoning with Sledgehammer and Metis
     1 (*  Title:      HOL/Metis_Examples/ROOT.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Testing Metis and Sledgehammer.
     6 *)
     7 
     8 use_thys ["set", "Abstraction", "BigO", "BT", "HO_Reas", "Message", "Tarski",
     9           "TransClosure"];