src/Pure/Isar/proof.ML

   val context_of: state -> context
   val theory_of: state -> theory
   val sign_of: state -> Sign.sg
   val map_context: (context -> context) -> state -> state
   val warn_extra_tfrees: state -> state -> state
+  val put_thms: string * thm list -> state -> state
   val reset_thms: string -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
   val get_goal: state -> context * (thm list * thm)
   val goal_facts: (state -> thm list) -> state -> state
-  val use_facts: state -> state
-  val reset_facts: state -> state
   val get_mode: state -> mode
   val is_chain: state -> bool
   val assert_forward: state -> state
   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state