equal
deleted
inserted
replaced
813 |
813 |
814 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
814 text{*Rewrites to push in Key and Crypt messages, so that other messages can |
815 be pulled out using the @{text analz_insert} rules*} |
815 be pulled out using the @{text analz_insert} rules*} |
816 ML |
816 ML |
817 {* |
817 {* |
818 fun insComm x y = inst "x" x (inst "y" y insert_commute); |
818 fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); |
819 |
819 |
820 bind_thms ("pushKeys", |
820 bind_thms ("pushKeys", |
821 map (insComm "Key ?K") |
821 map (insComm "Key ?K") |
822 ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", |
822 ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", |
823 "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); |
823 "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); |