equal
deleted
inserted
replaced
87 Rep o fa = fr o Rep & fa o Abs = Abs o fr" |
87 Rep o fa = fr o Rep & fa o Abs = Abs o fr" |
88 by (auto intro!: ext) |
88 by (auto intro!: ext) |
89 |
89 |
90 end |
90 end |
91 |
91 |
92 interpretation nat_int!: type_definition int nat "Collect (op <= 0)" |
92 interpretation nat_int: type_definition int nat "Collect (op <= 0)" |
93 by (rule td_nat_int) |
93 by (rule td_nat_int) |
94 |
94 |
95 declare |
95 declare |
96 nat_int.Rep_cases [cases del] |
96 nat_int.Rep_cases [cases del] |
97 nat_int.Abs_cases [cases del] |
97 nat_int.Abs_cases [cases del] |