1089 if is_quot_type thy (range_type T) then |
1089 if is_quot_type thy (range_type T) then |
1090 raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
1090 raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
1091 else |
1091 else |
1092 accum |> fold (add_nondef_axiom depth) |
1092 accum |> fold (add_nondef_axiom depth) |
1093 (nondef_props_for_const thy false nondef_table x) |
1093 (nondef_props_for_const thy false nondef_table x) |
1094 |> is_funky_typedef thy (range_type T) |
1094 |> (is_funky_typedef thy (range_type T) orelse |
|
1095 range_type T = nat_T) |
1095 ? fold (add_maybe_def_axiom depth) |
1096 ? fold (add_maybe_def_axiom depth) |
1096 (nondef_props_for_const thy true |
1097 (nondef_props_for_const thy true |
1097 (extra_table def_table s) x) |
1098 (extra_table def_table s) x) |
1098 else if is_rep_fun thy x then |
1099 else if is_rep_fun thy x then |
1099 if is_quot_type thy (domain_type T) then |
1100 if is_quot_type thy (domain_type T) then |
1100 raise NOT_SUPPORTED "\"Rep_\" function of quotient type" |
1101 raise NOT_SUPPORTED "\"Rep_\" function of quotient type" |
1101 else |
1102 else |
1102 accum |> fold (add_nondef_axiom depth) |
1103 accum |> fold (add_nondef_axiom depth) |
1103 (nondef_props_for_const thy false nondef_table x) |
1104 (nondef_props_for_const thy false nondef_table x) |
1104 |> is_funky_typedef thy (range_type T) |
1105 |> (is_funky_typedef thy (range_type T) orelse |
|
1106 range_type T = nat_T) |
1105 ? fold (add_maybe_def_axiom depth) |
1107 ? fold (add_maybe_def_axiom depth) |
1106 (nondef_props_for_const thy true |
1108 (nondef_props_for_const thy true |
1107 (extra_table def_table s) x) |
1109 (extra_table def_table s) x) |
1108 |> add_axioms_for_term depth |
1110 |> add_axioms_for_term depth |
1109 (Const (mate_of_rep_fun thy x)) |
1111 (Const (mate_of_rep_fun thy x)) |