equal
deleted
inserted
replaced
932 | _ => (if pred i then cv A else reflexive A, i+1) |
932 | _ => (if pred i then cv A else reflexive A, i+1) |
933 in combination (combination refl_implies thA) (gconv j B) end |
933 in combination (combination refl_implies thA) (gconv j B) end |
934 handle TERM _ => reflexive ct |
934 handle TERM _ => reflexive ct |
935 in gconv 1 end; |
935 in gconv 1 end; |
936 |
936 |
937 (* Rewrite A in !!x1,...x1. A *) |
937 (* Rewrite A in !!x1,...,xn. A *) |
938 fun forall_conv cv ct = |
938 fun forall_conv cv ct = |
939 let val p as (ct1, ct2) = Thm.dest_comb ct |
939 let val p as (ct1, ct2) = Thm.dest_comb ct |
940 in (case pairself term_of p of |
940 in (case pairself term_of p of |
941 (Const ("all", _), Abs (s, _, _)) => |
941 (Const ("all", _), Abs (s, _, _)) => |
942 let val (v, ct') = Thm.dest_abs (Some "@") ct2; |
942 let val (v, ct') = Thm.dest_abs (Some "@") ct2; |