more canonical name (2)
authornipkow
Wed Jun 19 10:14:50 2013 +0200 (2013-06-19)
changeset 52394fe33d456b36c
parent 52393 ba73041fd5b3
child 52395 7cc3f42930f3
more canonical name (2)
src/HOL/IMP/Denotational.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/IMP/Denotational.thy	Wed Jun 19 10:07:36 2013 +0200
     1.2 +++ b/src/HOL/IMP/Denotational.thy	Wed Jun 19 10:14:50 2013 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  
     1.5  header "Denotational Semantics of Commands"
     1.6  
     1.7 -theory Denotation imports Big_Step begin
     1.8 +theory Denotational imports Big_Step begin
     1.9  
    1.10  type_synonym com_den = "(state \<times> state) set"
    1.11  
     2.1 --- a/src/HOL/ROOT	Wed Jun 19 10:07:36 2013 +0200
     2.2 +++ b/src/HOL/ROOT	Wed Jun 19 10:14:50 2013 +0200
     2.3 @@ -119,7 +119,7 @@
     2.4      BExp
     2.5      ASM
     2.6      Finite_Reachable
     2.7 -    Denotation
     2.8 +    Denotational
     2.9      Comp_Rev
    2.10      Poly_Types
    2.11      Sec_Typing