Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: KeyMap.sml Sprache: Isabelle

Original von: Isabelle^©

theory Proc1
imports "HOL-SPARK.SPARK"
begin

spark_open \<open>loop_invariant/proc1\<close>

spark_vc procedure_proc1_5
  by (simp add: ring_distribs mod_simps)

spark_vc procedure_proc1_8
  by (simp add: ring_distribs mod_simps)

spark_end

lemma pow_2_32_simp: "4294967296 = (2::int)^32"
  by simp

end

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.