equal
deleted
inserted
replaced
20 end; |
20 end; |
21 |
21 |
22 structure Cla = ClassicalFun(Classical_Data); |
22 structure Cla = ClassicalFun(Classical_Data); |
23 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
23 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
24 |
24 |
25 ML_Context.value_antiq "claset" |
25 ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())"); |
26 (Scan.succeed ("claset", "Cla.local_claset_of (ML_Context.the_local_context ())")); |
|
27 |
26 |
28 |
27 |
29 (*Propositional rules*) |
28 (*Propositional rules*) |
30 val prop_cs = empty_cs |
29 val prop_cs = empty_cs |
31 addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI}, |
30 addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI}, @{thm impI}, |