Free SKILL.md scraped from GitHub. Clone the repo or copy the file directly into your Claude Code skills directory.
npx versuz@latest install a5c-ai-babysitter-library-specializations-domains-science-mathematics-skills-isabegit clone https://github.com/a5c-ai/babysitter.gitcp babysitter/SKILL.MD ~/.claude/skills/a5c-ai-babysitter-library-specializations-domains-science-mathematics-skills-isabe/SKILL.md--- name: isabelle-hol-interface description: Interface with Isabelle/HOL for classical mathematics formalization allowed-tools: - Bash - Read - Write - Edit - Glob - Grep metadata: specialization: mathematics domain: science category: theorem-proving phase: 6 --- # Isabelle/HOL Interface ## Purpose Provides expert guidance on using Isabelle/HOL for classical mathematics formalization and theorem proving. ## Capabilities - Isar structured proof generation - Sledgehammer automated theorem proving - Archive of Formal Proofs access - Locales and type classes - Code generation to SML/Haskell ## Usage Guidelines 1. **Isar Proofs**: Write structured proofs with have/show/proof 2. **Automation**: Use Sledgehammer for ATP assistance 3. **Libraries**: Access AFP for reusable formalizations 4. **Abstraction**: Use locales for modular theories ## Tools/Libraries - Isabelle - Archive of Formal Proofs (AFP) - Sledgehammer ATPs - Isabelle/jEdit