src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 61858 3f494c048142
parent 61770 a20048c78891
child 62342 1cf129590be8
equal deleted inserted replaced
61857:542f2c6da692 61858:3f494c048142
   572     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   572     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   573   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   573   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   574 
   574 
   575 fun dest_n_tuple 1 t = [t]
   575 fun dest_n_tuple 1 t = [t]
   576   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   576   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   577 
       
   578 type typedef_info =
       
   579   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
       
   580    prop_of_Rep: thm, set_name: string option, Abs_inverse: thm option,
       
   581    Rep_inverse: thm option}
       
   582 
   577 
   583 fun typedef_info ctxt s =
   578 fun typedef_info ctxt s =
   584   if is_frac_type ctxt (Type (s, [])) then
   579   if is_frac_type ctxt (Type (s, [])) then
   585     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   580     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   586           Abs_name = @{const_name Abs_Frac},
   581           Abs_name = @{const_name Abs_Frac},