equal
deleted
inserted
replaced
5 Extending of state setsExtending of state sets |
5 Extending of state setsExtending of state sets |
6 function f (forget) maps the extended state to the original state |
6 function f (forget) maps the extended state to the original state |
7 function g (forgotten) maps the extended state to the "extending part" |
7 function g (forgotten) maps the extended state to the "extending part" |
8 *) |
8 *) |
9 |
9 |
10 header{*Extending State Sets*} |
10 section{*Extending State Sets*} |
11 |
11 |
12 theory Extend imports Guar begin |
12 theory Extend imports Guar begin |
13 |
13 |
14 definition |
14 definition |
15 (*MOVE to Relation.thy?*) |
15 (*MOVE to Relation.thy?*) |