A Collection of Isabelle Programming Hacks
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Achim D. Brucker 76b983012d Added reminder to move configuration to Isabelle/Isar. 7 months ago
.ci Port to Isabelle 2019. 2 years ago
document Upgrading to Isabelle 2020. 9 months ago
fxp Changed ref to Unsynchronized.ref. 7 months ago
ml-yacc-lib Initial commit: ml-yacc support for Isabelle. 7 months ago
.gitignore Initial document generation support. 3 years ago
Assert.thy Port to Isabelle 2019. 2 years ago
Code_Reflection.thy Initial commit: SML Code Reflection 2 years ago
Hiding_Type_Variables.thy Port to Isabelle 2019. 2 years ago
LICENSE Initial commit. 4 years ago
Nano_JSON.thy Fixed serializer for definitions using equality from Pure. 3 years ago
README.md Fixed typo. 7 months ago
ROOT Integrated fxp and ml_yacc_lib. 7 months ago
example.json Added parser and overall cleanup. 3 years ago
fxp.thy Added reminder to move configuration to Isabelle/Isar. 7 months ago
ml_yacc_lib.thy Initial commit: ml-yacc support for Isabelle. 7 months ago


Isabelle Hacks

This project contains small Isabelle "hacks" that provide additional functionality to Isabelle or showcase specific functionality. The individual hacks usually consist out of a single theory file and all documentation is contained in that theory file. The master branch should work with the latest official release of Isabelle (Isabelle 2021, at time of writing), hacks for older versions might be available on a dedicated branch.

List of Isabelle Hacks

  • Assert.thy provides a new top level command assert that provides a simple way for specifying assertions that Isabelle checks while processing a theory.

  • Hiding_Type_Variables.thy provides print a setup for defining default type variables of type constructors. The default type variables can be hidden in output, e.g., ('a, 'b, 'c) foo is shown as (_) foo. This shorthand notation can also be used in input (using a parse translation), which (sometimes) helps to focus on the important parts of complex type declarations.

  • Nano_JSON.thy provides support for a JSON-like data exchange for Isabelle/HOL.

  • Code_Reflection.thy provides a new top-level command for reflecting generated SML code into Isabelle's ML environment.

  • ml_yacc_lib.thy provides Isabelle support for parser generated by ml-yacc (part of sml/NJ).

  • fxp.thy provides Isabelle support for The Functional XML Parser (fxp).


Main author: Achim D. Brucker


If not otherwise stated, all hacks are licensed under a 2-clause BSD-style license.

SPDX-License-Identifier: BSD-2-Clause

Master Repository

The master git repository for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/adbrucker/isabelle-hacks.