src/HOL/Statespace/StateFun.thy
changeset 25174 d70d6dbc3a60
parent 25171 4a9c25bffc9b
child 25408 156f6f7082b8
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Wed Oct 24 19:21:39 2007 +0200
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Wed Oct 24 19:21:40 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* State Space Representation as Function \label{sec:StateFun}*}
     1.5  
     1.6  theory StateFun imports DistinctTreeProver 
     1.7 -(*uses "state_space.ML" (state_fun)*)
     1.8 +(*uses "state_space.ML" ("state_fun.ML")*)
     1.9  begin
    1.10  
    1.11  
    1.12 @@ -109,7 +109,7 @@
    1.13    apply simp
    1.14    oops
    1.15  
    1.16 -(*use "state_fun"
    1.17 +(*use "state_fun.ML"
    1.18  setup StateFun.setup
    1.19  *)
    1.20  end
    1.21 \ No newline at end of file