| changeset 869 | ce5f78f0eac5 |
| parent 854 | 5961edda27d7 |
| child 870 | 2a19e0a37131 |
| 868:09d5b7f0e55d | 869:ce5f78f0eac5 |
|---|---|
93 term Quot_Type.abs |
93 term Quot_Type.abs |
94 |
94 |
95 section {* ML setup *} |
95 section {* ML setup *} |
96 |
96 |
97 (* Auxiliary data for the quotient package *) |
97 (* Auxiliary data for the quotient package *) |
98 |
|
98 use "quotient_info.ML" |
99 use "quotient_info.ML" |
99 |
100 |
100 declare [[map "fun" = (fun_map, fun_rel)]] |
101 declare [[map "fun" = (fun_map, fun_rel)]] |
101 |
102 |
102 lemmas [quot_thm] = fun_quotient |
103 lemmas [quot_thm] = fun_quotient |