equal
deleted
inserted
replaced
99 use "quotient_info.ML" |
99 use "quotient_info.ML" |
100 |
100 |
101 declare [[map "fun" = (fun_map, fun_rel)]] |
101 declare [[map "fun" = (fun_map, fun_rel)]] |
102 |
102 |
103 lemmas [quot_thm] = fun_quotient |
103 lemmas [quot_thm] = fun_quotient |
104 lemmas [quot_respect] = quot_rel_rsp bexeq_rsp |
104 lemmas [quot_respect] = quot_rel_rsp |
105 lemmas [quot_equiv] = identity_equivp |
105 lemmas [quot_equiv] = identity_equivp |
106 |
106 |
107 (* Lemmas about simplifying id's. *) |
107 (* Lemmas about simplifying id's. *) |
108 lemmas [id_simps] = |
108 lemmas [id_simps] = |
109 fun_map_id[THEN eq_reflection] |
109 fun_map_id[THEN eq_reflection] |