isabelle: src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy@64b47495676d (annotated)

45610 11095c312709 tuned header; wenzelm parents: 45065 diff changeset	1	(* Title: HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	2	Author: Stefan Berghofer
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	3	Copyright: secunet Security Networks AG
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	4	*)
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	5
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	6	theory Simple_Greatest_Common_Divisor
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 65552 diff changeset	7	imports SPARK
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	8	begin
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	9
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	10	spark_proof_functions
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	11	gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	12
56798 939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open berghofe parents: 45610 diff changeset	13	spark_open "simple_greatest_common_divisor/g_c_d"
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	14
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	15	spark_vc procedure_g_c_d_4
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58130 diff changeset	16	using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	17	by (simp add: gcd_non_0_int)
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	18
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	19	spark_vc procedure_g_c_d_9
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58130 diff changeset	20	using \<open>0 \<le> c\<close> \<open>gcd c 0 = gcd m n\<close>
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	21	by simp
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	22
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	23	spark_end
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	24
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	25	end

author	wenzelm
	Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787	64b47495676d
parent 66453	cc19f7ca2ed6
child 66992	69673025292e
permissions	-rw-r--r--