Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 49983 33e18e9916a8
parent 49914 23e36a4d28f1
child 50670 eaa540986291 
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -23,8 +23,9 @@
   val partial_type_encs : string list
   val metis_default_lam_trans : string
   val metis_call : string -> string -> string
+  val forall_of : term -> term -> term
+  val exists_of : term -> term -> term
   val unalias_type_enc : string -> string list
-  val forall_of : term -> term -> term
   val term_from_atp :
     Proof.context -> bool -> int Symtab.table -> typ option ->
     (string, string) ho_term -> term
isabelle