equal
deleted
inserted
replaced
58 structure Classical = ClassicalFun(Classical_Data); |
58 structure Classical = ClassicalFun(Classical_Data); |
59 |
59 |
60 structure BasicClassical: BASIC_CLASSICAL = Classical; |
60 structure BasicClassical: BASIC_CLASSICAL = Classical; |
61 |
61 |
62 open BasicClassical; |
62 open BasicClassical; |
63 val swap = Library.swap; |
|
64 |
63 |
65 val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" Classical.swap); |
64 val _ = bind_thm ("contrapos_np", inst "Pa" "?Q" Classical.swap); |
66 |
65 |
67 (*Propositional rules*) |
66 (*Propositional rules*) |
68 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
67 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |