Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Proc2.thy
Sprache: Isabelle
|
theory Proc2
imports "HOL-SPARK.SPARK"
begin
spark_open \<open>loop_invariant/proc2\<close>
spark_vc procedure_proc2_7
by (simp add: ring_distribs mod_simps)
spark_end
end
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
