| changeset 66992 | 69673025292e |
| parent 66453 | cc19f7ca2ed6 |
| child 69605 | a96320074298 |
| 66991:fc87d3becd69 | 66992:69673025292e |
|---|---|
2 Author: Stefan Berghofer |
2 Author: Stefan Berghofer |
3 Copyright: secunet Security Networks AG |
3 Copyright: secunet Security Networks AG |
4 *) |
4 *) |
5 |
5 |
6 theory Greatest_Common_Divisor |
6 theory Greatest_Common_Divisor |
7 imports SPARK |
7 imports "HOL-SPARK.SPARK" |
8 begin |
8 begin |
9 |
9 |
10 spark_proof_functions |
10 spark_proof_functions |
11 gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int" |
11 gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int" |
12 |
12 |