renamed rep_claset to rep_cs
authoroheimb
Wed Feb 25 20:29:58 1998 +0100 (1998-02-25)
changeset 4653d60f76680bf4
parent 4652 d24cca140eeb
child 4654 dbeae12ada20
renamed rep_claset to rep_cs
src/FOL/cladata.ML
src/FOLP/classical.ML
src/HOL/cladata.ML
src/Provers/blast.ML
src/Provers/classical.ML
     1.1 --- a/src/FOL/cladata.ML	Wed Feb 25 20:25:27 1998 +0100
     1.2 +++ b/src/FOL/cladata.ML	Wed Feb 25 20:29:58 1998 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    val dup_intr	= Cla.dup_intr
     1.5    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     1.6    val claset	= Cla.claset
     1.7 -  val rep_claset = Cla.rep_claset
     1.8 +  val rep_cs    = Cla.rep_cs
     1.9    end;
    1.10  
    1.11  structure Blast = BlastFun(Blast_Data);
     2.1 --- a/src/FOLP/classical.ML	Wed Feb 25 20:25:27 1998 +0100
     2.2 +++ b/src/FOLP/classical.ML	Wed Feb 25 20:29:58 1998 +0100
     2.3 @@ -41,7 +41,7 @@
     2.4    val addSEs: claset * thm list -> claset
     2.5    val addSIs: claset * thm list -> claset
     2.6    val print_cs: claset -> unit
     2.7 -  val rep_claset: claset -> 
     2.8 +  val rep_cs: claset -> 
     2.9        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
    2.10         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
    2.11         haz_brls: (bool*thm)list}
    2.12 @@ -102,7 +102,7 @@
    2.13          safep_brls: (bool*thm)list,
    2.14          haz_brls: (bool*thm)list};
    2.15    
    2.16 -fun rep_claset (CS x) = x;
    2.17 +fun rep_cs (CS x) = x;
    2.18  
    2.19  (*For use with biresolve_tac.  Combines intrs with swap to catch negated
    2.20    assumptions.  Also pairs elims with true. *)
     3.1 --- a/src/HOL/cladata.ML	Wed Feb 25 20:25:27 1998 +0100
     3.2 +++ b/src/HOL/cladata.ML	Wed Feb 25 20:29:58 1998 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4    val dup_intr	= Classical.dup_intr
     3.5    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     3.6    val claset	= Classical.claset
     3.7 -  val rep_claset = Classical.rep_claset
     3.8 +  val rep_cs    = Classical.rep_cs
     3.9    end;
    3.10  
    3.11  structure Blast = BlastFun(Blast_Data);
     4.1 --- a/src/Provers/blast.ML	Wed Feb 25 20:25:27 1998 +0100
     4.2 +++ b/src/Provers/blast.ML	Wed Feb 25 20:29:58 1998 +0100
     4.3 @@ -61,7 +61,7 @@
     4.4    val dup_intr		: thm -> thm
     4.5    val hyp_subst_tac     : bool ref -> int -> tactic
     4.6    val claset		: unit -> claset
     4.7 -  val rep_claset	: (* dependent on classical.ML *)
     4.8 +  val rep_cs	: (* dependent on classical.ML *)
     4.9        claset -> {safeIs: thm list, safeEs: thm list, 
    4.10  		 hazIs: thm list, hazEs: thm list,
    4.11  		 swrappers: (string * wrapper) list, 
    4.12 @@ -918,7 +918,7 @@
    4.13   "start" is CPU time at start, for printing search time
    4.14  *)
    4.15  fun prove (sign, start, cs, brs, cont) =
    4.16 - let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
    4.17 + let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
    4.18       val safeList = [safe0_netpair, safep_netpair]
    4.19       and hazList  = [haz_netpair]
    4.20       fun prv (tacs, trs, choices, []) = 
     5.1 --- a/src/Provers/classical.ML	Wed Feb 25 20:25:27 1998 +0100
     5.2 +++ b/src/Provers/classical.ML	Wed Feb 25 20:29:58 1998 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4    val empty_cs: claset
     5.5    val print_cs: claset -> unit
     5.6    val print_claset: theory -> unit
     5.7 -  val rep_claset: (* BLAST_DATA in blast.ML dependent on this *)
     5.8 +  val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
     5.9      claset -> {safeIs: thm list, safeEs: thm list,
    5.10  		 hazIs: thm list, hazEs: thm list,
    5.11  		 swrappers: (string * wrapper) list, 
    5.12 @@ -260,7 +260,7 @@
    5.13      Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs))
    5.14    end;
    5.15  
    5.16 -fun rep_claset (CS args) = args;
    5.17 +fun rep_cs (CS args) = args;
    5.18  
    5.19  local 
    5.20    fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);