TFL/rules.sig
changeset 3353 9112a2efb9a3
parent 3302 404fe31fd8d2
child 3379 7091ffa99c93
equal deleted inserted replaced
3352:04502e5431fb 3353:9112a2efb9a3
     7 *)
     7 *)
     8 
     8 
     9 signature Rules_sig =
     9 signature Rules_sig =
    10 sig
    10 sig
    11 (*  structure USyntax : USyntax_sig *)
    11 (*  structure USyntax : USyntax_sig *)
    12   type 'a binding
       
    13 
       
    14   val dest_thm : thm -> term list * term
    12   val dest_thm : thm -> term list * term
    15 
    13 
    16   (* Inference rules *)
    14   (* Inference rules *)
    17   val REFL      :cterm -> thm
    15   val REFL      :cterm -> thm
    18   val ASSUME    :cterm -> thm
    16   val ASSUME    :cterm -> thm
    21   val CONJUNCT1 :thm -> thm
    19   val CONJUNCT1 :thm -> thm
    22   val CONJUNCT2 :thm -> thm
    20   val CONJUNCT2 :thm -> thm
    23   val CONJUNCTS :thm -> thm list
    21   val CONJUNCTS :thm -> thm list
    24   val DISCH     :cterm -> thm -> thm
    22   val DISCH     :cterm -> thm -> thm
    25   val UNDISCH   :thm  -> thm
    23   val UNDISCH   :thm  -> thm
    26   val INST_TYPE :typ binding list -> thm -> thm
    24   val INST_TYPE :(typ*typ)list -> thm -> thm
    27   val SPEC      :cterm -> thm -> thm
    25   val SPEC      :cterm -> thm -> thm
    28   val ISPEC     :cterm -> thm -> thm
    26   val ISPEC     :cterm -> thm -> thm
    29   val ISPECL    :cterm list -> thm -> thm
    27   val ISPECL    :cterm list -> thm -> thm
    30   val GEN       :cterm -> thm -> thm
    28   val GEN       :cterm -> thm -> thm
    31   val GENL      :cterm list -> thm -> thm
    29   val GENL      :cterm list -> thm -> thm
    40   val PROVE_HYP : thm -> thm -> thm
    38   val PROVE_HYP : thm -> thm -> thm
    41 
    39 
    42   val CHOOSE : cterm * thm -> thm -> thm
    40   val CHOOSE : cterm * thm -> thm -> thm
    43   val EXISTS : cterm * cterm -> thm -> thm
    41   val EXISTS : cterm * cterm -> thm -> thm
    44   val EXISTL : cterm list -> thm -> thm
    42   val EXISTL : cterm list -> thm -> thm
    45   val IT_EXISTS : cterm binding list -> thm -> thm
    43   val IT_EXISTS : (cterm*cterm) list -> thm -> thm
    46 
    44 
    47   val EVEN_ORS : thm list -> thm list
    45   val EVEN_ORS : thm list -> thm list
    48   val DISJ_CASESL : thm -> thm list -> thm
    46   val DISJ_CASESL : thm -> thm list -> thm
    49 
    47 
    50   val SUBS : thm list -> thm -> thm
    48   val SUBS : thm list -> thm -> thm