equal
deleted
inserted
replaced
76 |
76 |
77 (*** Proof theory of propositional logic ***) |
77 (*** Proof theory of propositional logic ***) |
78 |
78 |
79 structure PropThms = Inductive_Fun |
79 structure PropThms = Inductive_Fun |
80 (val thy = PropLog.thy; |
80 (val thy = PropLog.thy; |
|
81 val thy_name = "PropThms"; |
81 val rec_doms = [("thms","prop")]; |
82 val rec_doms = [("thms","prop")]; |
82 val sintrs = |
83 val sintrs = |
83 ["[| p:H; p:prop |] ==> H |- p", |
84 ["[| p:H; p:prop |] ==> H |- p", |
84 "[| p:prop; q:prop |] ==> H |- p=>q=>p", |
85 "[| p:prop; q:prop |] ==> H |- p=>q=>p", |
85 "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r", |
86 "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r", |