src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
changeset 56798 939e88e79724
parent 45610 11095c312709
child 58130 5e9170812356
equal deleted inserted replaced
56797:32963b43a538 56798:939e88e79724
     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