src/Pure/thm.ML
changeset 16135 c66545fe72bf
parent 16024 ffe25459c72a
child 16287 7a03b4b4df67
equal deleted inserted replaced
16134:89ea482e1649 16135:c66545fe72bf
    46                                   shyps: sort list, hyps: cterm list, 
    46                                   shyps: sort list, hyps: cterm list, 
    47                                   tpairs: (cterm * cterm) list, prop: cterm}
    47                                   tpairs: (cterm * cterm) list, prop: cterm}
    48   exception THM of string * int * thm list
    48   exception THM of string * int * thm list
    49   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
    49   type 'a attribute 	(* = 'a * thm -> 'a * thm *)
    50   val eq_thm		: thm * thm -> bool
    50   val eq_thm		: thm * thm -> bool
       
    51   val eq_thms		: thm list * thm list -> bool
    51   val sign_of_thm       : thm -> Sign.sg
    52   val sign_of_thm       : thm -> Sign.sg
    52   val prop_of           : thm -> term
    53   val prop_of           : thm -> term
    53   val proof_of		: thm -> Proofterm.proof
    54   val proof_of		: thm -> Proofterm.proof
    54   val transfer_sg	: Sign.sg -> thm -> thm
    55   val transfer_sg	: Sign.sg -> thm -> thm
    55   val transfer		: theory -> thm -> thm
    56   val transfer		: theory -> thm -> thm
   339     Sorts.eq_set_sort (shyps1, shyps2) andalso
   340     Sorts.eq_set_sort (shyps1, shyps2) andalso
   340     aconvs (hyps1, hyps2) andalso
   341     aconvs (hyps1, hyps2) andalso
   341     aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
   342     aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
   342     prop1 aconv prop2
   343     prop1 aconv prop2
   343   end;
   344   end;
       
   345 
       
   346 val eq_thms = Library.equal_lists eq_thm;
   344 
   347 
   345 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   348 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   346 fun prop_of (Thm {prop, ...}) = prop;
   349 fun prop_of (Thm {prop, ...}) = prop;
   347 fun proof_of (Thm {der = (_, proof), ...}) = proof;
   350 fun proof_of (Thm {der = (_, proof), ...}) = proof;
   348 
   351