src/HOL/Relation.ML
changeset 1465 5d7a7e439cec
parent 1454 d0266c81a85e
child 1552 6f71b5d46700
     1.1 --- a/src/HOL/Relation.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/Relation.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title: 	Relation.ML
     1.5 +(*  Title:      Relation.ML
     1.6      ID:         $Id$
     1.7 -    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     1.8 -        	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9 +    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
    1.10 +                Lawrence C Paulson, Cambridge University Computer Laboratory
    1.11      Copyright   1994 Universita' di Firenze
    1.12      Copyright   1993  University of Cambridge
    1.13  *)
    1.14 @@ -100,7 +100,7 @@
    1.15      (assume_tac 1) ]);
    1.16  
    1.17  val converse_cs = comp_cs addSIs [converseI] 
    1.18 -			  addSEs [converseD,converseE];
    1.19 +                          addSEs [converseD,converseE];
    1.20  
    1.21  (** Domain **)
    1.22  
    1.23 @@ -138,13 +138,13 @@
    1.24  qed_goal "Image_singleton_iff" Relation.thy
    1.25      "(b : r^^{a}) = ((a,b):r)"
    1.26   (fn _ => [ rtac (Image_iff RS trans) 1,
    1.27 -	    fast_tac comp_cs 1 ]);
    1.28 +            fast_tac comp_cs 1 ]);
    1.29  
    1.30  qed_goalw "ImageI" Relation.thy [Image_def]
    1.31      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
    1.32   (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
    1.33              (resolve_tac [conjI ] 1),
    1.34 -            (resolve_tac [RangeI] 1),
    1.35 +            (rtac RangeI 1),
    1.36              (REPEAT (fast_tac set_cs 1))]);
    1.37  
    1.38  qed_goalw "ImageE" Relation.thy [Image_def]