doc-src/Dirs
author blanchet
Wed, 28 Apr 2010 16:05:38 +0200
changeset 36494 2478dd225b68
parent 33191 fe3c65d9c577
child 36926 90bb12cf8e36
permissions -rw-r--r--
add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)

Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main