equal
deleted
inserted
replaced
5 |
5 |
6 Datatype definition of propositional logic formulae and inductive definition |
6 Datatype definition of propositional logic formulae and inductive definition |
7 of the propositional tautologies. |
7 of the propositional tautologies. |
8 *) |
8 *) |
9 |
9 |
10 PropLog = Finite + Univ + |
10 PropLog = Finite + Datatype + |
11 |
11 |
12 (** The datatype of propositions; note mixfix syntax **) |
12 (** The datatype of propositions; note mixfix syntax **) |
13 consts |
13 consts |
14 prop :: "i" |
14 prop :: "i" |
15 |
15 |