# HG changeset patch # User wenzelm # Date 1186512216 -7200 # Node ID c89d77d97f84d60b83d2046555c5120a6b6986d7 # Parent 4ff1dc2aa18dedbb8c269caba6bd1263c844c74d fixed imports from ../../Auth; diff -r 4ff1dc2aa18d -r c89d77d97f84 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Aug 07 20:19:55 2007 +0200 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Tue Aug 07 20:43:36 2007 +0200 @@ -8,7 +8,7 @@ header{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*} -theory NSP_Bad imports "../Auth/Public" "../UNITY_Main" begin +theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin text{*This is the flawed version, vulnerable to Lowe's attack. From page 260 of