equal
deleted
inserted
replaced
9 Spriner LNCS 1586 (1999), pages 1215-1227. |
9 Spriner LNCS 1586 (1999), pages 1215-1227. |
10 *) |
10 *) |
11 |
11 |
12 header{*A Family of Similar Counters: Original Version*} |
12 header{*A Family of Similar Counters: Original Version*} |
13 |
13 |
14 theory Counter = UNITY_Main: |
14 theory Counter imports UNITY_Main begin |
15 |
15 |
16 (* Variables are names *) |
16 (* Variables are names *) |
17 datatype name = C | c nat |
17 datatype name = C | c nat |
18 types state = "name=>int" |
18 types state = "name=>int" |
19 |
19 |