src/HOL/Relation.ML
changeset 4089 96fba19bcbe2
parent 3718 d78cf498a88c
child 4423 a129b817b58a
     1.1 --- a/src/HOL/Relation.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -178,11 +178,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 (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.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];