equal
deleted
inserted
replaced
31 (* |
31 (* |
32 ML {* set Lin_Arith.trace; *} |
32 ML {* set Lin_Arith.trace; *} |
33 *) |
33 *) |
34 |
34 |
35 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, |
35 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, |
36 @{term HOL.minus}, @{term nat}, @{term Divides.mod}, |
36 @{term Algebras.minus}, @{term nat}, @{term Divides.mod}, |
37 @{term Divides.div} *} |
37 @{term Divides.div} *} |
38 |
38 |
39 lemma "(i::nat) <= max i j" |
39 lemma "(i::nat) <= max i j" |
40 by linarith |
40 by linarith |
41 |
41 |