equal
deleted
inserted
replaced
7 apply(rule equivpI) |
7 apply(rule equivpI) |
8 unfolding reflp_def symp_def transp_def |
8 unfolding reflp_def symp_def transp_def |
9 apply(auto) |
9 apply(auto) |
10 done |
10 done |
11 |
11 |
|
12 print_quotients |
|
13 |
|
14 ML{* |
|
15 Quotient_Info.quotient_rules_get @{context} |
|
16 *} |
|
17 |
12 fun |
18 fun |
13 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
19 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
14 where |
20 where |
15 "intrel (x, y) (u, v) = (x + v = u + y)" |
21 "intrel (x, y) (u, v) = (x + v = u + y)" |
16 |
22 |
17 quotient_type int = "nat \<times> nat" / intrel |
23 quotient_type int = "nat \<times> nat" / intrel |
18 sorry |
24 sorry |
|
25 |
|
26 print_quotients |
19 |
27 |
20 ML {* |
28 ML {* |
21 open Quotient_Term; |
29 open Quotient_Term; |
22 *} |
30 *} |
23 |
31 |