equal
deleted
inserted
replaced
55 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) |
55 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) |
56 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
56 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
57 |
57 |
58 AddSIs [ballI]; |
58 AddSIs [ballI]; |
59 AddEs [ballE]; |
59 AddEs [ballE]; |
|
60 AddXDs [bspec]; |
60 (* gives better instantiation for bound: *) |
61 (* gives better instantiation for bound: *) |
61 claset_ref() := claset() addWrapper ("bspec", fn tac2 => |
62 claset_ref() := claset() addWrapper ("bspec", fn tac2 => |
62 (dtac bspec THEN' atac) APPEND' tac2); |
63 (dtac bspec THEN' atac) APPEND' tac2); |
63 |
64 |
64 (*Normally the best argument order: P(x) constrains the choice of x:A*) |
65 (*Normally the best argument order: P(x) constrains the choice of x:A*) |