Skip to content

Commit a200146

Browse files
committed
don't change theories
1 parent ff58d08 commit a200146

1 file changed

Lines changed: 0 additions & 2 deletions

File tree

theories/crypto/RndExcept.eca

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -141,8 +141,6 @@ abstract theory Adversary.
141141
proof.
142142
proc.
143143
call (_: SampleB.bad, ={SampleB.bad}, ={SampleB.bad}); 1: apply A_ll.
144-
admit.
145-
move => &m2. hsample.
146144
+ proc=> /=; sp 1 1; if => //;inline *.
147145
seq 3 3 : (={r0,i0,X0,SampleB.bad} /\ (test i0 X0){1} /\ !SampleB.bad{2}); 1: by auto.
148146
wp;if{1}; 2 : by auto => /#.

0 commit comments

Comments
 (0)