| changeset 29509 | 1ff0f3f08a7b |
| parent 29248 | f1f1bccf2fc5 |
| child 38838 | 62f6ba39b3d4 |
--- a/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 08:29:11 2009 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Fri Jan 16 14:58:11 2009 +0100 @@ -41,7 +41,7 @@ projection~/ injection functions that convert from abstract values to @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *} -class_locale vars' = +locale vars' = fixes n::'name and b::'name assumes "distinct [n, b]"