Skip to content

Commit 0a08d4a

Browse files
author
Andrei Popescu
committed
more on readme
1 parent 8db0434 commit 0a08d4a

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

README.md

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,9 @@ Counterexample 16 --> theorem `counterexample` from No_Least_Support_Counterexam
169169

170170
Thm 19 --> theorem `strong_induct` (in locale `Induct`) from thys/Generic_Strong_Rule_Induction.thy.
171171

172-
Prop 20 --> theorem `affine.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinary_Lambda_Calculus/ILC_affine.thy 1234
172+
Prop 20 --> theorem `affine.strong_induct` (generated and proved by `binder_inductive`) from thys/Infinary_Lambda_Calculus/ILC_affine.thy
173+
174+
Prop 21 --> theorem `strong_induct_reneqv` from ILC_Renaming_Equivalence.thy
173175

174176
Thm 22 --> theorem `strong_iinduct` (in locale `IInduct`) from thys/Generic_Strong_Rule_Induction.thy.
175177

0 commit comments

Comments
 (0)