src/Provers/quasi.ML
changeset 19250 932a50e2332f
parent 15570 8d8c70b41bab
child 22578 b0eb5652f210
     1.1 --- a/src/Provers/quasi.ML	Sat Mar 11 17:30:35 2006 +0100
     1.2 +++ b/src/Provers/quasi.ML	Sat Mar 11 21:23:10 2006 +0100
     1.3 @@ -61,9 +61,9 @@
     1.4         where Rel is one of "<", "<=", "=" and "~=",
     1.5         other relation symbols cause an error message *)
     1.6    (* decomp_trans is used by trans_tac, it may only return Rel = "<=" *)
     1.7 -  val decomp_trans: Sign.sg -> term -> (term * string * term) option
     1.8 +  val decomp_trans: theory -> term -> (term * string * term) option
     1.9    (* decomp_quasi is used by quasi_tac *)
    1.10 -  val decomp_quasi: Sign.sg -> term -> (term * string * term) option
    1.11 +  val decomp_quasi: theory -> term -> (term * string * term) option
    1.12  end;
    1.13  
    1.14  signature QUASI_TAC = 
    1.15 @@ -117,7 +117,7 @@
    1.16  
    1.17  (* ************************************************************************ *)
    1.18  (*                                                                          *)
    1.19 -(* mkasm_trans sign (t, n) :  Sign.sg -> (Term.term * int)  -> less         *)
    1.20 +(* mkasm_trans sign (t, n) :  theory -> (Term.term * int)  -> less          *)
    1.21  (*                                                                          *)
    1.22  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    1.23  (* translated to an element of type less.                                   *)
    1.24 @@ -136,7 +136,7 @@
    1.25    
    1.26  (* ************************************************************************ *)
    1.27  (*                                                                          *)
    1.28 -(* mkasm_quasi sign (t, n) : Sign.sg -> (Term.term * int) -> less           *)
    1.29 +(* mkasm_quasi sign (t, n) : theory -> (Term.term * int) -> less            *)
    1.30  (*                                                                          *)
    1.31  (* Tuple (t, n) (t an assumption, n its index in the assumptions) is        *)
    1.32  (* translated to an element of type less.                                   *)
    1.33 @@ -163,7 +163,7 @@
    1.34  
    1.35  (* ************************************************************************ *)
    1.36  (*                                                                          *)
    1.37 -(* mkconcl_trans sign t : Sign.sg -> Term.term -> less                      *)
    1.38 +(* mkconcl_trans sign t : theory -> Term.term -> less                       *)
    1.39  (*                                                                          *)
    1.40  (* Translates conclusion t to an element of type less.                      *)
    1.41  (* Only for Conclusions of form x <= y or x < y.                            *)
    1.42 @@ -181,7 +181,7 @@
    1.43    
    1.44  (* ************************************************************************ *)
    1.45  (*                                                                          *)
    1.46 -(* mkconcl_quasi sign t : Sign.sg -> Term.term -> less                      *)
    1.47 +(* mkconcl_quasi sign t : theory -> Term.term -> less                       *)
    1.48  (*                                                                          *)
    1.49  (* Translates conclusion t to an element of type less.                      *)
    1.50  (* Quasi orders only.                                                       *)
    1.51 @@ -504,7 +504,7 @@
    1.52  (* *********************************************************************** *)
    1.53  (*                                                                         *)
    1.54  (* solveLeTrans sign (asms,concl) :                                        *)
    1.55 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    1.56 +(* theory -> less list * Term.term -> proof list                           *)
    1.57  (*                                                                         *)
    1.58  (* Solves                                                                  *)
    1.59  (*                                                                         *)
    1.60 @@ -527,7 +527,7 @@
    1.61  (* *********************************************************************** *)
    1.62  (*                                                                         *)
    1.63  (* solveQuasiOrder sign (asms,concl) :                                     *)
    1.64 -(* Sign.sg -> less list * Term.term -> proof list                          *)
    1.65 +(* theory -> less list * Term.term -> proof list                           *)
    1.66  (*                                                                         *)
    1.67  (* Find proof if possible for quasi order.                                 *)
    1.68  (*                                                                         *)