publish a private function
authorkuncar
Mon, 13 May 2013 12:13:24 +0200
changeset 51954 2e3f9e72b8c4
parent 51953 ae755fd6c883
child 51955 04d9381bebff
publish a private function
src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Mon May 13 06:50:37 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
@@ -9,6 +9,7 @@
   val prep_conv: conv
   val get_relator_eq: Proof.context -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
+  val get_relator_eq_raw: Proof.context -> thm list
   val get_transfer_raw: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute