tuned signature: more exports;
authorwenzelm
Mon, 10 Jun 2024 20:23:42 +0200
changeset 80331 6f25a035069c
parent 80330 e01aae620437
child 80332 4bed658a01fc
tuned signature: more exports;
src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Jun 10 14:53:54 2024 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Jun 10 20:23:42 2024 +0200
@@ -17,6 +17,7 @@
   }
   val query_parser: (bool * string criterion) list parser
   val read_query: Position.T -> string -> (bool * string criterion) list
+  val all_facts_of: Proof.context -> (Thm_Name.T * thm) list
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * term criterion) list -> int option * (Thm_Name.T * thm) list
   val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->