src/HOL/Statespace/StateFun.thy
 changeset 25408 156f6f7082b8 parent 25174 d70d6dbc3a60 child 35114 b1fd1d756e20
equal 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
    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
   115 end
   111 end