changeset 2563 | e908e2716f3a |
parent 2326 | 6df4488339e4 |
child 3511 | da4dd8b7ced4 |
2562:d571d6660240 | 2563:e908e2716f3a |
---|---|
12 val banner = "Security Protocols"; |
12 val banner = "Security Protocols"; |
13 writeln banner; |
13 writeln banner; |
14 |
14 |
15 init_thy_reader(); |
15 init_thy_reader(); |
16 |
16 |
17 (*Must be redefined in order to refer to the new instance of bind_thm |
|
18 created by init_thy_reader.*) |
|
19 fun qed_spec_mp name = |
|
20 let val thm = normalize_thm [RSspec,RSmp] (result()) |
|
21 in bind_thm(name, thm) end; |
|
22 |
|
23 use_thy "Message"; |
17 use_thy "Message"; |
24 |
18 |