equal
deleted
inserted
replaced
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 |
13 spark_open "simple_greatest_common_divisor/g_c_d.siv" |
13 spark_open "simple_greatest_common_divisor/g_c_d" |
14 |
14 |
15 spark_vc procedure_g_c_d_4 |
15 spark_vc procedure_g_c_d_4 |
16 using `0 < d` `gcd c d = gcd m n` |
16 using `0 < d` `gcd c d = gcd m n` |
17 by (simp add: gcd_non_0_int) |
17 by (simp add: gcd_non_0_int) |
18 |
18 |