| changeset 9619 | 6125cc9efc18 |
| parent 9066 | b1e874e38dab |
| child 10212 | 33fe2d701ddd |
| 9618:ff8238561394 | 9619:6125cc9efc18 |
|---|---|
7 basis for theory ToyList in the documentation. |
7 basis for theory ToyList in the documentation. |
8 *) |
8 *) |
9 |
9 |
10 theory PreList = |
10 theory PreList = |
11 Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + |
11 Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + |
12 SVC_Oracle: |
12 SVC_Oracle + While: |
13 |
13 |
14 theorems [cases type: bool] = case_split |
14 theorems [cases type: bool] = case_split |
15 |
15 |
16 end |
16 end |