# HG changeset patch
# User wenzelm
# Date 965256289 -7200
# Node ID e5857656b8f0163ee6b446bc6ff9e8b869ceb945
# Parent  09c75c801dde21075f66ad6e363f1e161287616e
export get_local_clasimpset, clasimp_modifiers;

diff -r 09c75c801dde -r e5857656b8f0 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Aug 03 00:44:08 2000 +0200
+++ b/src/Provers/clasimp.ML	Thu Aug 03 00:44:49 2000 +0200
@@ -47,6 +47,8 @@
   val force	  : int -> unit
   val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
   val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
+  val get_local_clasimpset: Proof.context -> clasimpset
+  val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val setup	  : (theory -> theory) list
 end;