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