src/HOL/Relation.ML
changeset 4650 91af1ef45d68
parent 4644 ecf8f17f6fe0
child 4673 59d80bacee62
     1.1 --- a/src/HOL/Relation.ML	Wed Feb 25 15:45:32 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Wed Feb 25 15:48:04 1998 +0100
     1.3 @@ -215,11 +215,11 @@
     1.4      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
     1.5  
     1.6  goal Relation.thy "R O id = R";
     1.7 -by (fast_tac (claset() addbefore split_all_tac) 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "R_O_id";
    1.10  
    1.11  goal Relation.thy "id O R = R";
    1.12 -by (fast_tac (claset() addbefore split_all_tac) 1);
    1.13 +by (Fast_tac 1);
    1.14  qed "id_O_R";
    1.15  
    1.16  Addsimps [R_O_id,id_O_R];