equal
deleted
inserted
replaced
1 theory IntEx2 |
1 theory IntEx2 |
2 imports "../QuotMain" |
2 imports "../QuotMain" |
3 uses |
3 (*uses |
4 ("Tools/numeral.ML") |
4 ("Tools/numeral.ML") |
5 ("Tools/numeral_syntax.ML") |
5 ("Tools/numeral_syntax.ML") |
6 ("Tools/int_arith.ML") |
6 ("Tools/int_arith.ML")*) |
7 begin |
7 begin |
8 |
8 |
9 |
9 |
10 fun |
10 fun |
11 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
11 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |