src/HOL/Statespace/StateFun.thy
 changeset 25174 d70d6dbc3a60 parent 25171 4a9c25bffc9b child 25408 156f6f7082b8
equal inserted replaced
25173:7e1f197a36c5 25174:d70d6dbc3a60
     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)*)
     9 (*uses "state_space.ML" ("state_fun.ML")*)
    10 begin
    10 begin
    11
    11
    12
    12
    13 text {* The state space is represented as a function from names to
    13 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
    14 values. We neither fix the type of names nor the type of values. We
   107   apply (simp add: update_def lookup_def)
   107   apply (simp add: update_def lookup_def)
   108   apply (rule ext)
   108   apply (rule ext)
   109   apply simp
   109   apply simp
   110   oops
   110   oops
   111
   111
   112 (*use "state_fun"
   112 (*use "state_fun.ML"
   113 setup StateFun.setup
   113 setup StateFun.setup
   114 *)
   114 *)
   115 end
   115 end