Isabelle-extreme

| Feature | isabelle-extreme | Isabelle/HOL | |---------|--------------------|---------------| | Logic | Minimal equational logic + fixed point | Higher-order logic | | Types | Simple types (no type classes) | Rich types with type classes | | Recursion | Via fixed point combinator ( fix ) | Primitive recursion, well-founded recursion | | Automation | None (manual rewriting only) | simp , auto , blast , sledgehammer | | Code generation | No | Yes (to ML, Scala, Haskell) | | Library | Empty | Thousands of theorems |

If you’ve ever wondered, “What is the absolute minimum logic needed to build an ITP?” – isabelle-extreme is your answer. isabelle-extreme

theory Scratch imports Main begin (* Define addition via fixed point *) definition add :: "nat ⇒ nat ⇒ nat" where "add ≡ fix (λadd n m. if n = 0 then m else add (n-1) (m+1))" isabelle-extreme