# HG changeset patch
# User kuncar
# Date 1444347869 -7200
# Node ID 15adc37aa851991868d2695e856f3208e8702871
# Parent  33a62b54f381815e0f039d4e03e995515597d4e4
documentation for transfer debug methods

diff -r 33a62b54f381 -r 15adc37aa851 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Oct 09 01:44:27 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Oct 09 01:44:29 2015 +0200
@@ -1603,6 +1603,11 @@
     @{method_def (HOL) "transfer_prover"} & : & @{text method} \\
     @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
     @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
+    @{method_def (HOL) "transfer_start"} & : & @{text method} \\
+    @{method_def (HOL) "transfer_prover_start"} & : & @{text method} \\
+    @{method_def (HOL) "transfer_step"} & : & @{text method} \\
+    @{method_def (HOL) "transfer_end"} & : & @{text method} \\
+    @{method_def (HOL) "transfer_prover_end"} & : & @{text method} \\
     @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
     @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
     @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
@@ -1629,6 +1634,17 @@
   terms of other constants that already have transfer rules. It should be
   applied after unfolding the constant definitions.
 
+  \item @{method (HOL) "transfer_start"}, @{method (HOL) "transfer_step"},
+  @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"}
+  and @{method (HOL) "transfer_prover_end"} methods are meant to be used
+  for debugging of @{method (HOL) "transfer"} and @{method (HOL) "transfer_prover"},
+  which we can decompose as follows:
+  @{method (HOL) "transfer"} = (@{method (HOL) "transfer_start"}, 
+  @{method (HOL) "transfer_step"}+, @{method (HOL) "transfer_end"}) and
+  @{method (HOL) "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, 
+  @{method (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}).
+  For usage examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"} 
+
   \item @{attribute (HOL) "untransferred"} proves the same equivalent
   theorem as @{method (HOL) "transfer"} internally does.