more on readme

Andrei Popescu · Andrei Popescu · commit f76aec238b03 · 2024-10-16T12:14:55.000+01:00
diff --git a/README.md b/README.md
@@ -201,9 +201,13 @@ Thm. 29 --> just a recallection of the standard rule induction of the predicate
 
 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`
 
+##### Appendix B
 
+Prop 34 --> theorem `cong.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinitary_FOL/Pi_cong.thy
 
+Prop 35 --> theorem `trans.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinitary_FOL/Pi_trans.thy
 
+Lemma 36 --> the sublocale statement `sublocale NominalSet < LSNominalSet` from thys/Generic_Strong_Rule_Induction.thy
 
 
 
diff --git a/thys/Urban_Berghofer_Norrish_Rule_Induction.thy b/thys/Urban_Berghofer_Norrish_Rule_Induction.thy
@@ -268,4 +268,6 @@ by (auto simp: Tperm_id Tperm_comp' G_mono)
 
 
 
+
+
 end

Original file line number	Diff line number	Diff line change
`@@ -268,4 +268,6 @@ by (auto simp: Tperm_id Tperm_comp' G_mono)`
`268`	`268`
`269`	`269`
`270`	`270`
	`271`	`+`
	`272`	`+`
`271`	`273`	`end`