src/HOL/Statespace/StateFun.thy
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