14 val MINOR = "minor" |
14 val MINOR = "minor" |
15 val CONTROL = "control" |
15 val CONTROL = "control" |
16 val DIAG = "diag" |
16 val DIAG = "diag" |
17 val THY_BEGIN = "thy_begin" |
17 val THY_BEGIN = "thy_begin" |
18 val THY_END = "thy_end" |
18 val THY_END = "thy_end" |
19 val THY_HEADING = "thy_heading" |
19 val THY_HEADING1 = "thy_heading1" |
|
20 val THY_HEADING2 = "thy_heading2" |
|
21 val THY_HEADING3 = "thy_heading3" |
|
22 val THY_HEADING4 = "thy_heading4" |
20 val THY_DECL = "thy_decl" |
23 val THY_DECL = "thy_decl" |
21 val THY_SCRIPT = "thy_script" |
24 val THY_SCRIPT = "thy_script" |
22 val THY_GOAL = "thy_goal" |
25 val THY_GOAL = "thy_goal" |
23 val THY_SCHEMATIC_GOAL = "thy_schematic_goal" |
26 val THY_SCHEMATIC_GOAL = "thy_schematic_goal" |
24 val QED = "qed" |
27 val QED = "qed" |
25 val QED_BLOCK = "qed_block" |
28 val QED_BLOCK = "qed_block" |
26 val QED_GLOBAL = "qed_global" |
29 val QED_GLOBAL = "qed_global" |
27 val PRF_HEADING = "prf_heading" |
30 val PRF_HEADING2 = "prf_heading2" |
|
31 val PRF_HEADING3 = "prf_heading3" |
|
32 val PRF_HEADING4 = "prf_heading4" |
28 val PRF_GOAL = "prf_goal" |
33 val PRF_GOAL = "prf_goal" |
29 val PRF_BLOCK = "prf_block" |
34 val PRF_BLOCK = "prf_block" |
30 val PRF_OPEN = "prf_open" |
35 val PRF_OPEN = "prf_open" |
31 val PRF_CLOSE = "prf_close" |
36 val PRF_CLOSE = "prf_close" |
32 val PRF_CHAIN = "prf_chain" |
37 val PRF_CHAIN = "prf_chain" |
40 |
45 |
41 val minor = Set(MINOR) |
46 val minor = Set(MINOR) |
42 val control = Set(CONTROL) |
47 val control = Set(CONTROL) |
43 val diag = Set(DIAG) |
48 val diag = Set(DIAG) |
44 val theory = |
49 val theory = |
45 Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL) |
50 Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, |
|
51 THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL) |
46 val theory1 = Set(THY_BEGIN, THY_END) |
52 val theory1 = Set(THY_BEGIN, THY_END) |
47 val theory2 = Set(THY_DECL, THY_GOAL) |
53 val theory2 = Set(THY_DECL, THY_GOAL) |
48 val proof = |
54 val proof = |
49 Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK, |
55 Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL, |
50 PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT) |
56 PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT) |
51 val proof1 = |
57 val proof1 = |
52 Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL) |
58 Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL) |
53 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL) |
59 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL) |
54 val improper = Set(THY_SCRIPT, PRF_SCRIPT) |
60 val improper = Set(THY_SCRIPT, PRF_SCRIPT) |
55 } |
61 } |