conj_intr_list and conj_elim_precise: cover 0 conjuncts;
authorwenzelm
Tue Jan 15 00:09:29 2002 +0100 (2002-01-15)
changeset 1275608bf3d911968
parent 12755 a906a8b364f1
child 12757 b76a4376cfcb
conj_intr_list and conj_elim_precise: cover 0 conjuncts;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jan 15 00:08:51 2002 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Jan 15 00:09:29 2002 +0100
     1.3 @@ -923,7 +923,9 @@
     1.4  in
     1.5  
     1.6  fun conj_intr tha thb = thb COMP (tha COMP incr [tha, thb] conj_intr_rule);
     1.7 -val conj_intr_list = foldr1 (uncurry conj_intr);
     1.8 +
     1.9 +fun conj_intr_list [] = asm_rl
    1.10 +  | conj_intr_list ths = foldr1 (uncurry conj_intr) ths;
    1.11  
    1.12  fun conj_elim th =
    1.13    let val th' = forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th
    1.14 @@ -933,7 +935,8 @@
    1.15    let val (th1, th2) = conj_elim th
    1.16    in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th];
    1.17  
    1.18 -fun conj_elim_precise 1 th = [th]
    1.19 +fun conj_elim_precise 0 _ = []
    1.20 +  | conj_elim_precise 1 th = [th]
    1.21    | conj_elim_precise n th =
    1.22        let val (th1, th2) = conj_elim th
    1.23        in th1 :: conj_elim_precise (n - 1) th2 end;