equal
deleted
inserted
replaced
19 Fin(H)"} |
19 Fin(H)"} |
20 *} |
20 *} |
21 |
21 |
22 subsection {* The datatype of propositions *} |
22 subsection {* The datatype of propositions *} |
23 |
23 |
24 datatype |
24 datatype 'a pl = |
25 'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90) |
25 false | |
|
26 var 'a ("#_" [1000]) | |
|
27 imp "'a pl" "'a pl" (infixr "->" 90) |
26 |
28 |
27 subsection {* The proof system *} |
29 subsection {* The proof system *} |
28 |
30 |
29 inductive |
31 inductive |
30 thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50) |
32 thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50) |