|Achim D. Brucker faae943ad9 Fixed serializer for definitions using equality from Pure.||4 months ago|
|.ci||4 months ago|
|document||4 months ago|
|.gitignore||4 months ago|
|Assert.thy||4 months ago|
|Hiding_Type_Variables.thy||4 months ago|
|LICENSE||1 year ago|
|Nano_JSON.thy||4 months ago|
|README.md||4 months ago|
|ROOT||4 months ago|
|example.json||4 months ago|
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 2018, at time of writing), hacks for older versions might be available on a dedicated branch.
Assert.thy provides a new top level command assert that provides a simple way for specifying assertions that Isabelle checks while processing a theory.
print a setup for defining default type variables of type
constructors. The default type variables can be hidden in output,
('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
Nano_JSON.thy provides support for a JSON-like data exchange for Isabelle/HOL.
Main author: Achim D. Brucker
If not otherwise stated, all hacks are licensed under a 2-clause BSD-style license.
The master git repository for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/adbrucker/isabelle-hacks.