src/HOL/Statespace/StateSpaceEx.thy
changeset 29247 95d3a82857e5
parent 29235 2d62b637fa80
child 29248 f1f1bccf2fc5
     1.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Tue Dec 16 21:11:39 2008 +0100
     1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Dec 18 11:16:48 2008 +0100
     1.3 @@ -30,6 +30,10 @@
     1.4    n::nat
     1.5    b::bool
     1.6  
     1.7 +print_locale vars_namespace
     1.8 +print_locale vars_valuetypes
     1.9 +print_locale vars
    1.10 +
    1.11  text {* \noindent This resembles a \isacommand{record} definition, 
    1.12  but introduces sophisticated locale
    1.13  infrastructure instead of HOL type schemes.  The resulting context
    1.14 @@ -196,18 +200,25 @@
    1.15    by simp
    1.16  
    1.17  
    1.18 +text {* Hmm, I hoped this would work now...*}
    1.19 +
    1.20 +locale fooX = foo +
    1.21 + assumes "s<a:=i>\<cdot>b = k"
    1.22 +
    1.23 +(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *)
    1.24  text {* There are known problems with syntax-declarations. They currently
    1.25  only work, when the context is already built. Hopefully this will be 
    1.26  implemented correctly in future Isabelle versions. *}
    1.27  
    1.28 +(*
    1.29  lemma 
    1.30    assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
    1.31    shows True
    1.32  proof
    1.33 -  class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
    1.34 +  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
    1.35    term "s<a := i>\<cdot>a = i"
    1.36  qed
    1.37 -
    1.38 +*)
    1.39  (*
    1.40  lemma 
    1.41    includes foo