src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 33699 f33b036ef318
parent 33583 b5e0909cd5ea
child 33701 9dd1079cec3a
equal deleted inserted replaced
33698:b5f36fa5a7b4 33699:f33b036ef318
   187             codatatypes: (string * (string * styp list)) list}
   187             codatatypes: (string * (string * styp list)) list}
   188   val empty = {frac_types = [], codatatypes = []}
   188   val empty = {frac_types = [], codatatypes = []}
   189   val extend = I
   189   val extend = I
   190   fun merge ({frac_types = fs1, codatatypes = cs1},
   190   fun merge ({frac_types = fs1, codatatypes = cs1},
   191                {frac_types = fs2, codatatypes = cs2}) : T =
   191                {frac_types = fs2, codatatypes = cs2}) : T =
   192     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
   192     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
   193      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
   193      codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
   194 
   194 
   195 (* term * term -> term *)
   195 (* term * term -> term *)
   196 fun s_conj (t1, @{const True}) = t1
   196 fun s_conj (t1, @{const True}) = t1
   197   | s_conj (@{const True}, t2) = t2
   197   | s_conj (@{const True}, t2) = t2
   198   | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
   198   | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}