removed obsolete mk_conjunction_list, intr/elim_list;
authorwenzelm
Tue Jul 03 17:17:09 2007 +0200 (2007-07-03)
changeset 2353558147e5bd070
parent 23534 3f82d1798976
child 23536 60a1672e298e
removed obsolete mk_conjunction_list, intr/elim_list;
src/Pure/conjunction.ML
     1.1 --- a/src/Pure/conjunction.ML	Tue Jul 03 17:17:09 2007 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Tue Jul 03 17:17:09 2007 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  sig
     1.5    val conjunction: cterm
     1.6    val mk_conjunction: cterm * cterm -> cterm
     1.7 -  val mk_conjunction_list: cterm list -> cterm
     1.8    val mk_conjunction_balanced: cterm list -> cterm
     1.9    val dest_conjunction: cterm -> cterm * cterm
    1.10    val cong: thm -> thm -> thm
    1.11 @@ -18,10 +17,8 @@
    1.12    val conjunctionD2: thm
    1.13    val conjunctionI: thm
    1.14    val intr: thm -> thm -> thm
    1.15 -  val intr_list: thm list -> thm
    1.16    val intr_balanced: thm list -> thm
    1.17    val elim: thm -> thm * thm
    1.18 -  val elim_list: thm -> thm list
    1.19    val elim_balanced: int -> thm -> thm list
    1.20    val curry_balanced: int -> thm -> thm
    1.21    val uncurry_balanced: int -> thm -> thm
    1.22 @@ -40,9 +37,6 @@
    1.23  
    1.24  fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    1.25  
    1.26 -fun mk_conjunction_list [] = true_prop
    1.27 -  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    1.28 -
    1.29  fun mk_conjunction_balanced [] = true_prop
    1.30    | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
    1.31  
    1.32 @@ -114,18 +108,11 @@
    1.33  end;
    1.34  
    1.35  
    1.36 -(* multiple conjuncts *)
    1.37 -
    1.38 -fun intr_list [] = asm_rl
    1.39 -  | intr_list ths = foldr1 (uncurry intr) ths;
    1.40 +(* balanced conjuncts *)
    1.41  
    1.42  fun intr_balanced [] = asm_rl
    1.43    | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
    1.44  
    1.45 -fun elim_list th =   (* FIXME improper!? rename to "elims" *)
    1.46 -  let val (th1, th2) = elim th
    1.47 -  in elim_list th1 @ elim_list th2 end handle THM _ => [th];
    1.48 -
    1.49  fun elim_balanced 0 _ = []
    1.50    | elim_balanced n th = BalancedTree.dest elim n th;
    1.51