Isabelle-dL

(★ 8)

A formally verified implementation of differential dynamic logic in Isabelle

Owner Repos

KeYmaeraX-release ★ 101

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)

Scala
Coq-dL ★ 21

A formally verified implementation of differential dynamic logic in Coq

Coq
KeYmaeraX-projects ★ 8

Projects, models, and proofs in KeYmaera X

Shell

File Explorer

ZIP Download
  • .gitignore
  • Axioms.thy
  • Bound_Effect.thy
  • Codegen-Exploder.thy
  • Codegen_Example.thy
  • Codegen_Exploder.thy
  • Coincidence.thy
  • Denotational_Semantics.thy
  • Differential_Axioms.thy
  • Differential_Axioms2.thy
  • Differential_Dynamic_Logic.thy
  • Example_DIAnd.thy
  • Example_System.thy
  • Finite_String.thy
  • Frechet_Correctness.thy
  • Ids.thy
  • Interval_Arithmetic.thy
  • Interval_Rat.thy
  • Lib.thy
  • Lib.thy~
  • Notation_HOL.thy
  • Notation_Word.thy
  • Pretty_Printer.thy
  • Proof_Checker.thy
  • README.md
  • ROOT
  • Scratch.thy
  • Static_Semantics.thy
  • Syntax.thy
  • Uniform_Renaming.thy
  • USubst.thy
  • USubst_Lemma.thy

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Link
Example
// repository documentation