more on readme

Author: Andrei Popescu

README.md

@@ -152,8 +152,11 @@ As discussed in Sect. 9 and App. G, we have automated the production of binding-
 
 ### Mapping of the results from the paper to Isabelle theorem names
 
+
 #### For the main paper 
 
+##### Appendix A
+
 Prop 1 --> subsumed by Prop. 2 (also generated and proved automatically by the standard inductive definition)
 
 Prop 2 --> theorem `step.strong_induct` (generated and proved by `binder_inductive`) from thys/Untyped_Lambda_Calculus
@@ -178,13 +181,18 @@ Prop 21 --> theorem `strong_induct_reneqv` from ILC_Renaming_Equivalence.thy
 
 Thm 22 --> theorem `strong_iinduct` (in locale `IInduct`) from thys/Generic_Strong_Rule_Induction.thy. 
 
+
 #### For the appendix
 
+##### Appendix A
+
+The Urban-Berghofer-Norrish result described in App. A is formalized in an incremental sequence of locales that follows the same structere and naming as the locales for our main abstract results. `UBN` stands for the acronym of the author names.
+
 Thm. 29 --> just a recallection of the standard rule induction of the predicate generated by the rules. In isabelle the predicate is called `II` and is located in thys/Urban_Berghofer_Norrish_Rule_Induction.thy, in the locale `UBN_Components`, so the Isabelle is called `II.induct`.
 
 Thm. 33 --> this is infered from our Thm. 19 (theorem `strong_induct` in locale `Induct`) via a sublocale relationship: `UBN < UBN: Induct_simple` (the second `UBN` is just a label to avoid name clashes), which makes the theorem `strong_induct` available into the locale `UBN` 
 
-(NB: The Urban-Berghofer-Norrish result is formalized in an incremental sequence of locales that follows the same structere and naming as the locales for our main abstract results. `UBN` stands for the acronym of the author names.)
+