src/HOL/UNITY/Constrains.thy
changeset 32960 69916a850301
parent 23767 7272a839ccd9
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      HOL/UNITY/Constrains
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/UNITY/Constrains.thy
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1998  University of Cambridge
     1.9  
    1.10 @@ -21,7 +20,7 @@
    1.11      Init:  "s \<in> init ==> (s,[]) \<in> traces init acts"
    1.12  
    1.13    | Acts:  "[| act: acts;  (s,evs) \<in> traces init acts;  (s,s'): act |]
    1.14 -	    ==> (s', s#evs) \<in> traces init acts"
    1.15 +            ==> (s', s#evs) \<in> traces init acts"
    1.16  
    1.17  
    1.18  inductive_set
    1.19 @@ -31,7 +30,7 @@
    1.20      Init:  "s \<in> Init F ==> s \<in> reachable F"
    1.21  
    1.22    | Acts:  "[| act: Acts F;  s \<in> reachable F;  (s,s'): act |]
    1.23 -	    ==> s' \<in> reachable F"
    1.24 +            ==> s' \<in> reachable F"
    1.25  
    1.26  constdefs
    1.27    Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co" 60)