# HG changeset patch
# User wenzelm
# Date 1718043822 -7200
# Node ID 6f25a035069c6f71a945c381ddf1d9facfcf4272
# Parent  e01aae6204372b258950038b67dceda361b81329
tuned signature: more exports;

diff -r e01aae620437 -r 6f25a035069c 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 ->