| changeset 8551 | 5c22595bc599 |
| parent 8201 | a81d18b0a9b1 |
| child 9180 | 3bda56c0d70d |
--- a/src/ZF/CardinalArith.ML Wed Mar 22 12:33:34 2000 +0100 +++ b/src/ZF/CardinalArith.ML Wed Mar 22 12:45:41 2000 +0100 @@ -291,7 +291,7 @@ Goal "Card(n) ==> 2 |*| n = n |+| n"; by (asm_simp_tac (simpset() addsimps [cmult_succ_lemma, Card_is_Ord, - read_instantiate [("j","0")] cadd_commute]) 1); + inst "j" "0" cadd_commute]) 1); qed "cmult_2";