src/HOL/Statespace/StateFun.thy
changeset 25408 156f6f7082b8
parent 25174 d70d6dbc3a60
child 35114 b1fd1d756e20
     1.1 --- a/src/HOL/Statespace/StateFun.thy	Sun Nov 11 20:29:07 2007 +0100
     1.2 +++ b/src/HOL/Statespace/StateFun.thy	Mon Nov 12 11:07:22 2007 +0100
     1.3 @@ -6,7 +6,6 @@
     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.ML")*)
     1.8  begin
     1.9  
    1.10  
    1.11 @@ -109,7 +108,4 @@
    1.12    apply simp
    1.13    oops
    1.14  
    1.15 -(*use "state_fun.ML"
    1.16 -setup StateFun.setup
    1.17 -*)
    1.18  end
    1.19 \ No newline at end of file