tuned rotate_prems;
authorwenzelm
Tue Jul 03 17:17:11 2007 +0200 (2007-07-03)
changeset 23537ecf487dce798
parent 23536 60a1672e298e
child 23538 438e5c4ef2c0
tuned rotate_prems;
tuned comments;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jul 03 17:17:11 2007 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 03 17:17:11 2007 +0200
     1.3 @@ -443,7 +443,9 @@
     1.4   end;
     1.5  
     1.6  (*Rotates a rule's premises to the left by k*)
     1.7 -val rotate_prems = permute_prems 0;
     1.8 +fun rotate_prems 0 = I
     1.9 +  | rotate_prems k = permute_prems 0 k;
    1.10 +
    1.11  fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
    1.12  
    1.13  (* permute prems, where the i-th position in the argument list (counting from 0)
    1.14 @@ -585,8 +587,8 @@
    1.15  
    1.16  val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
    1.17  
    1.18 -fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM*)
    1.19 -fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM*)
    1.20 +fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM in LCF/HOL*)
    1.21 +fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM in LCF/HOL*)
    1.22  
    1.23  local
    1.24    val dest_eq = Thm.dest_equals o cprop_of