equal
deleted
inserted
replaced
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 |