Isabelle2018: Resources
linkes
introduction
course
blog
cheat sheet
best practice
meta-logic
code generation
type class
Pure
locale
HOL
function
proof
isar
automation
by contradiction
Others
mailing list
Hereditary Harrop Formulas
definition
CryptHOL
Game-based proofs for cryptographic protocols in Isabelle/HOL
type
https://gyazo.com/669289276d84a0dc663257bbeb0d256e
term
https://gyazo.com/136c0aab7eda769927a1ba6b7f8e3ba5
formulae
https://gyazo.com/7618fbcefbbd5c7e69073824a00c017e