| changeset 22862 | 3dd306cb98d2 |
| parent 21828 | b8166438c772 |
| child 23891 | 4127c1d910f1 |
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML Tue May 08 05:30:10 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML Tue May 08 08:21:39 2007 +0200 @@ -13,7 +13,7 @@ (*** Basic properties of pubK & priK ***) -AddIffs [inj_pubK RS inj_eq]; +AddIffs [inj_pubK RS @{thm inj_eq}]; Goal "(priK A = priK B) = (A=B)"; by Safe_tac;