equal
deleted
inserted
replaced
12 val keysFor_def = thm "keysFor_def"; |
12 val keysFor_def = thm "keysFor_def"; |
13 val parts_mono = thm "parts_mono"; |
13 val parts_mono = thm "parts_mono"; |
14 val analz_mono = thm "analz_mono"; |
14 val analz_mono = thm "analz_mono"; |
15 val synth_mono = thm "synth_mono"; |
15 val synth_mono = thm "synth_mono"; |
16 val HPair_def = thm "HPair_def"; |
16 val HPair_def = thm "HPair_def"; |
17 val isSymKey_def = thm "isSymKey_def"; |
17 val symKeys_def = thm "symKeys_def"; |
18 |
18 |
19 structure parts = |
19 structure parts = |
20 struct |
20 struct |
21 val induct = thm "parts.induct"; |
21 val induct = thm "parts.induct"; |
22 val Inj = thm "parts.Inj"; |
22 val Inj = thm "parts.Inj"; |