equal
deleted
inserted
replaced
6 header {* The division operators div and mod *} |
6 header {* The division operators div and mod *} |
7 |
7 |
8 theory Divides |
8 theory Divides |
9 imports Nat_Transfer |
9 imports Nat_Transfer |
10 begin |
10 begin |
11 |
|
12 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" |
|
13 |
11 |
14 subsection {* Syntactic division operations *} |
12 subsection {* Syntactic division operations *} |
15 |
13 |
16 class div = dvd + |
14 class div = dvd + |
17 fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70) |
15 fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70) |