equal
deleted
inserted
replaced
10 quotient_type |
10 quotient_type |
11 my_int = "nat \<times> nat" / intrel |
11 my_int = "nat \<times> nat" / intrel |
12 apply(unfold equivp_def) |
12 apply(unfold equivp_def) |
13 apply(auto simp add: mem_def expand_fun_eq) |
13 apply(auto simp add: mem_def expand_fun_eq) |
14 done |
14 done |
15 |
|
16 thm quot_equiv |
|
17 |
|
18 thm quot_thm |
|
19 |
|
20 thm my_int_equivp |
|
21 |
|
22 print_theorems |
|
23 print_quotients |
|
24 |
15 |
25 quotient_definition |
16 quotient_definition |
26 "ZERO :: my_int" |
17 "ZERO :: my_int" |
27 as |
18 as |
28 "(0::nat, 0::nat)" |
19 "(0::nat, 0::nat)" |