isabelle: src/HOL/SPARK/Manual/Proc2.thy@a11ebc8c751a (annotated)

45044 2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	1	theory Proc2
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/proc2\<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_proc2_7
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_end
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	11
2fae15f8984d Added documentation for HOL-SPARK berghofe parents: diff changeset	12	end