src/HOL/Statespace/StateFun.thy
changeset 25408 156f6f7082b8
parent 25174 d70d6dbc3a60
child 35114 b1fd1d756e20
equal deleted inserted replaced
25407:2859cf34aaf0 25408:156f6f7082b8
     4 *)
     4 *)
     5 
     5 
     6 header {* State Space Representation as Function \label{sec:StateFun}*}
     6 header {* State Space Representation as Function \label{sec:StateFun}*}
     7 
     7 
     8 theory StateFun imports DistinctTreeProver 
     8 theory StateFun imports DistinctTreeProver 
     9 (*uses "state_space.ML" ("state_fun.ML")*)
       
    10 begin
     9 begin
    11 
    10 
    12 
    11 
    13 text {* The state space is represented as a function from names to
    12 text {* The state space is represented as a function from names to
    14 values. We neither fix the type of names nor the type of values. We
    13 values. We neither fix the type of names nor the type of values. We
   107   apply (simp add: update_def lookup_def)
   106   apply (simp add: update_def lookup_def)
   108   apply (rule ext)
   107   apply (rule ext)
   109   apply simp
   108   apply simp
   110   oops
   109   oops
   111 
   110 
   112 (*use "state_fun.ML"
       
   113 setup StateFun.setup
       
   114 *)
       
   115 end
   111 end