src/Pure/thm.ML
changeset 16024 ffe25459c72a
parent 15797 a63605582573
child 16135 c66545fe72bf
equal deleted inserted replaced
16023:66561f6814bd 16024:ffe25459c72a
   298   shyps: sort list,            (*sort hypotheses*)
   298   shyps: sort list,            (*sort hypotheses*)
   299   hyps: term list,             (*hypotheses*)
   299   hyps: term list,             (*hypotheses*)
   300   tpairs: (term * term) list,  (*flex-flex pairs*)
   300   tpairs: (term * term) list,  (*flex-flex pairs*)
   301   prop: term};                 (*conclusion*)
   301   prop: term};                 (*conclusion*)
   302 
   302 
   303 fun terms_of_tpairs tpairs = List.concat (map (op @ o pairself single) tpairs);
   303 fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs);
   304 
   304 
   305 fun attach_tpairs tpairs prop =
   305 fun attach_tpairs tpairs prop =
   306   Logic.list_implies (map Logic.mk_equals tpairs, prop);
   306   Logic.list_implies (map Logic.mk_equals tpairs, prop);
   307 
   307 
   308 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   308 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =