src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 45980 af59825c40cf
parent 45797 977cf00fb8d3
child 46081 8f6465f7021b
equal deleted inserted replaced
45979:296d9a9c8d24 45980:af59825c40cf
   543 
   543 
   544 fun typedef_info ctxt s =
   544 fun typedef_info ctxt s =
   545   if is_frac_type ctxt (Type (s, [])) then
   545   if is_frac_type ctxt (Type (s, [])) then
   546     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   546     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   547           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   547           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   548           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   548           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
   549                           |> Logic.varify_global,
   549                           |> Logic.varify_global,
   550           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   550           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   551   else case Typedef.get_info ctxt s of
   551   else case Typedef.get_info ctxt s of
   552     (* When several entries are returned, it shouldn't matter much which one
   552     (* When several entries are returned, it shouldn't matter much which one
   553        we take (according to Florian Haftmann). *)
   553        we take (according to Florian Haftmann). *)