equal
deleted
inserted
replaced
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Meta-theory of propositional logic *} |
7 header {* Meta-theory of propositional logic *} |
8 |
8 |
9 theory PropLog = Main: |
9 theory PropLog imports Main begin |
10 |
10 |
11 text {* |
11 text {* |
12 Datatype definition of propositional logic formulae and inductive |
12 Datatype definition of propositional logic formulae and inductive |
13 definition of the propositional tautologies. |
13 definition of the propositional tautologies. |
14 |
14 |