lucas - added more comments and an extra type to clarify the code.
authordixon
Sun Feb 27 00:00:40 2005 +0100 (2005-02-27)
changeset 15550806214035275
parent 15549 14d167259812
child 15551 af78481b37bf
lucas - added more comments and an extra type to clarify the code.
src/Provers/eqsubst.ML
     1.1 --- a/src/Provers/eqsubst.ML	Wed Feb 23 15:19:00 2005 +0100
     1.2 +++ b/src/Provers/eqsubst.ML	Sun Feb 27 00:00:40 2005 +0100
     1.3 @@ -27,6 +27,12 @@
     1.4  signature EQSUBST_TAC = 
     1.5  sig
     1.6  
     1.7 +  type match = 
     1.8 +       ((Term.indexname * Term.typ) list (* type instantiations *)
     1.9 +         * (Term.indexname * Term.term) list) (* term instantiations *)
    1.10 +        * (string * Term.typ) list (* type abs env *)
    1.11 +        * Term.term (* outer term *)
    1.12 +
    1.13    val prep_subst_in_asm :
    1.14        (Sign.sg (* sign for matching *)
    1.15         -> int (* maxidx *)
    1.16 @@ -61,10 +67,7 @@
    1.17            * int (* num of premises of asm *) 
    1.18            * Thm.thm) (* premthm *)
    1.19        -> Thm.thm (* rule *)
    1.20 -      -> (((Term.indexname * Term.typ) list (* type instantiations *)
    1.21 -          * (Term.indexname * Term.term) list) (* term instantiations *)
    1.22 -         * (string * Term.typ) list (* type abs env *)
    1.23 -         * Term.term) (* outer term *)
    1.24 +      -> match
    1.25        -> Thm.thm Seq.seq
    1.26  
    1.27    val prep_concl_subst :
    1.28 @@ -80,10 +83,7 @@
    1.29             * Thm.thm  (* trivial thm of goal concl *)
    1.30              (* possible matches/unifiers *)
    1.31          -> Thm.thm (* rule *)
    1.32 -        -> (((Term.indexname * Term.typ) list (* type instantiations *)
    1.33 -              * (Term.indexname * Term.term) list ) (* term instantiations *)
    1.34 -             * (string * Term.typ) list (* Type abs env *)
    1.35 -             * Term.term) (* outer term *)
    1.36 +        -> match
    1.37          -> Thm.thm Seq.seq (* substituted goal *)
    1.38  
    1.39    val eqsubst_asm_meth : Thm.thm list -> Proof.method
    1.40 @@ -102,6 +102,14 @@
    1.41    : EQSUBST_TAC
    1.42  = struct
    1.43  
    1.44 +  (* a type abriviation for match infomration *)
    1.45 +  type match = 
    1.46 +       ((Term.indexname * Term.typ) list (* type instantiations *)
    1.47 +         * (Term.indexname * Term.term) list) (* term instantiations *)
    1.48 +        * (string * Term.typ) list (* type abs env *)
    1.49 +        * Term.term (* outer term *)
    1.50 +
    1.51 +
    1.52  (* FOR DEBUGGING...
    1.53  type trace_subst_errT = int (* subgoal *)
    1.54          * Thm.thm (* thm with all goals *)