isabelle: src/HOL/SPARK/Manual/Proc1.thy@abf3e80bd815 (annotated)

45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	1	theory Proc1
66992 69673025292e less global theories -- avoid confusion about special cases; wenzelm parents: 66453 diff changeset	2	imports "HOL-SPARK.SPARK"
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	3	begin
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	4
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66992 diff changeset	5	spark_open \<open>loop_invariant/proc1\<close>
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	6
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	7	spark_vc procedure_proc1_5
64593 50c715579715 reoriented congruence rules in non-explosive direction haftmann parents: 58130 diff changeset	8	by (simp add: ring_distribs mod_simps)
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	9
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	10	spark_vc procedure_proc1_8
64593 50c715579715 reoriented congruence rules in non-explosive direction haftmann parents: 58130 diff changeset	11	by (simp add: ring_distribs mod_simps)
45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	12
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	13	spark_end
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	14
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	15	lemma pow_2_32_simp: "4294967296 = (2::int)^32"
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	16	by simp
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	17
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	18	end

author	wenzelm
	Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751	abf3e80bd815
parent 69605	a96320074298
permissions	-rw-r--r--