src/HOL/Statespace/StateSpaceEx.thy
changeset 29235 2d62b637fa80
parent 28611 983c1855a7af
child 29247 95d3a82857e5
     1.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Dec 15 18:12:52 2008 +0100
     1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Tue Dec 16 15:09:12 2008 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  projection~/ injection functions that convert from abstract values to
     1.5  @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
     1.6  
     1.7 -locale vars' =
     1.8 +class_locale vars' =
     1.9    fixes n::'name and b::'name
    1.10    assumes "distinct [n, b]" 
    1.11  
    1.12 @@ -204,7 +204,7 @@
    1.13    assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
    1.14    shows True
    1.15  proof
    1.16 -  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
    1.17 +  class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
    1.18    term "s<a := i>\<cdot>a = i"
    1.19  qed
    1.20