| changeset 58825 | 2065f49da190 |
| parent 48891 | c0eafbd55de3 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 17:01:44 2014 +0100 @@ -10,7 +10,6 @@ ML_file "state_space.ML" ML_file "state_fun.ML" -setup StateFun.setup text {* For every type that is to be stored in a state space, an instance of this locale is imported in order convert the abstract and