src/HOL/IMP/Denotation.thy
changeset 41589 bbd861837ebc
parent 34055 fdf294ee08b2
child 42174 d0be2722ce9f
equal deleted inserted replaced
41588:9546828c0eb3 41589:bbd861837ebc
     1 (*  Title:      HOL/IMP/Denotation.thy
     1 (*  Title:      HOL/IMP/Denotation.thy
     2     ID:         $Id$
       
     3     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     2     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     4     Copyright   1994 TUM
       
     5 *)
     3 *)
     6 
     4 
     7 header "Denotational Semantics of Commands"
     5 header "Denotational Semantics of Commands"
     8 
     6 
     9 theory Denotation imports Natural begin
     7 theory Denotation imports Natural begin