42 val PRF_SCRIPT = "prf_script" |
42 val PRF_SCRIPT = "prf_script" |
43 |
43 |
44 |
44 |
45 /* categories */ |
45 /* categories */ |
46 |
46 |
47 val minor = Set(MINOR) |
47 val diag = Set(DIAG) |
48 val control = Set(CONTROL) |
48 val control = Set(CONTROL) |
49 val diag = Set(DIAG) |
49 |
|
50 val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, |
|
51 PRF_HEADING2, PRF_HEADING3, PRF_HEADING4) |
|
52 |
50 val theory = |
53 val theory = |
51 Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, |
54 Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, |
52 THY_DECL, THY_GOAL) |
55 THY_DECL, THY_GOAL) |
53 val theory1 = Set(THY_BEGIN, THY_END) |
56 val theory1 = Set(THY_BEGIN, THY_END) |
54 val theory2 = Set(THY_DECL, THY_GOAL) |
57 val theory2 = Set(THY_DECL, THY_GOAL) |
|
58 val theory_body = |
|
59 Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL) |
|
60 |
55 val proof = |
61 val proof = |
56 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, |
62 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, |
57 PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, |
63 PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, |
58 PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
64 PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
59 val proof1 = |
65 val proof1 = |
60 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
66 Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, |
61 PRF_CHAIN, PRF_DECL) |
67 PRF_CHAIN, PRF_DECL) |
62 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) |
68 val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) |
|
69 |
|
70 val proof_body = |
|
71 Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, |
|
72 PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) |
|
73 |
|
74 val theory_goal = Set(THY_GOAL) |
|
75 val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) |
|
76 val qed = Set(QED, QED_SCRIPT, QED_BLOCK) |
|
77 val qed_global = Set(QED_GLOBAL) |
63 } |
78 } |
64 |
79 |