equal
deleted
inserted
replaced
13 section {* Constants *} |
13 section {* Constants *} |
14 |
14 |
15 text {* Most constants are already declared by HOL. *} |
15 text {* Most constants are already declared by HOL. *} |
16 |
16 |
17 consts |
17 consts |
18 assoc :: "['a::times, 'a] => bool" (infixl 50) |
18 assoc :: "['a::times, 'a] => bool" (infixl "assoc" 50) |
19 irred :: "'a::{zero, one, times} => bool" |
19 irred :: "'a::{zero, one, times} => bool" |
20 prime :: "'a::{zero, one, times} => bool" |
20 prime :: "'a::{zero, one, times} => bool" |
21 |
21 |
22 section {* Axioms *} |
22 section {* Axioms *} |
23 |
23 |