equal
deleted
inserted
replaced
9 - variables can be quantified over. |
9 - variables can be quantified over. |
10 *) |
10 *) |
11 |
11 |
12 header{*UNITY Program States*} |
12 header{*UNITY Program States*} |
13 |
13 |
14 theory State = Main: |
14 theory State imports Main begin |
15 |
15 |
16 consts var :: i |
16 consts var :: i |
17 datatype var = Var("i \<in> list(nat)") |
17 datatype var = Var("i \<in> list(nat)") |
18 type_intros nat_subset_univ [THEN list_subset_univ, THEN subsetD] |
18 type_intros nat_subset_univ [THEN list_subset_univ, THEN subsetD] |
19 |
19 |