src/HOL/Relation.ML
changeset 2637 e9b203f854ae
parent 2031 03a843f0f447
child 2891 d8f254ad1ab9
     1.1 --- a/src/HOL/Relation.ML	Sat Feb 15 17:48:19 1997 +0100
     1.2 +++ b/src/HOL/Relation.ML	Sat Feb 15 17:52:31 1997 +0100
     1.3 @@ -173,11 +173,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);
     1.8 +by (fast_tac (!claset addbefore split_all_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);
    1.13 +by (fast_tac (!claset addbefore split_all_tac) 1);
    1.14  qed "id_O_R";
    1.15  
    1.16  Addsimps [R_O_id,id_O_R];