changeset 25174 | d70d6dbc3a60 |
parent 25171 | 4a9c25bffc9b |
child 25408 | 156f6f7082b8 |
--- a/src/HOL/Statespace/StateFun.thy Wed Oct 24 19:21:39 2007 +0200 +++ b/src/HOL/Statespace/StateFun.thy Wed Oct 24 19:21:40 2007 +0200 @@ -6,7 +6,7 @@ header {* State Space Representation as Function \label{sec:StateFun}*} theory StateFun imports DistinctTreeProver -(*uses "state_space.ML" (state_fun)*) +(*uses "state_space.ML" ("state_fun.ML")*) begin @@ -109,7 +109,7 @@ apply simp oops -(*use "state_fun" +(*use "state_fun.ML" setup StateFun.setup *) end \ No newline at end of file