changeset 39887 | 74939e2afb95 |
parent 39886 | 8a9f0c97d550 |
child 39893 | 25a339e1ff9b |
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 22:23:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 23:06:02 2010 +0200 @@ -13,6 +13,7 @@ val trace : bool Unsynchronized.ref val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a + val untyped_aconv : term -> term -> bool val replay_one_inference : Proof.context -> mode -> (string * term) list -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list