src/HOL/Relation.ML
changeset 5316 7a8975451a89
parent 5231 2a454140ae24
child 5335 07fb8999de62
     1.1 --- a/src/HOL/Relation.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  by (Blast_tac 1);
     1.5  qed "idI";
     1.6  
     1.7 -val major::prems = goalw thy [id_def]
     1.8 +val major::prems = Goalw [id_def]
     1.9      "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
    1.10  \    |] ==>  P";  
    1.11  by (rtac (major RS CollectE) 1);
    1.12 @@ -34,7 +34,7 @@
    1.13  qed "compI";
    1.14  
    1.15  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.16 -val prems = goalw thy [comp_def]
    1.17 +val prems = Goalw [comp_def]
    1.18      "[| xz : r O s;  \
    1.19  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    1.20  \    |] ==> P";
    1.21 @@ -43,7 +43,7 @@
    1.22       ORELSE ares_tac prems 1));
    1.23  qed "compE";
    1.24  
    1.25 -val prems = goal thy
    1.26 +val prems = Goal
    1.27      "[| (a,c) : r O s;  \
    1.28  \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
    1.29  \    |] ==> P";
    1.30 @@ -78,7 +78,7 @@
    1.31  
    1.32  (** Natural deduction for trans(r) **)
    1.33  
    1.34 -val prems = goalw thy [trans_def]
    1.35 +val prems = Goalw [trans_def]
    1.36      "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
    1.37  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.38  qed "transI";