A Collection of Isabelle Programming Hacks
Go to file
Achim D. Brucker f2566edeec
adbrucker/isabelle-hacks/master This commit looks good Details
Initial commit: SML Code Reflection
2019-08-15 20:48:07 +01:00
.ci Port to Isabelle 2019. 2019-06-23 00:15:50 +01:00
document Port to Isabelle 2019. 2019-06-23 00:15:50 +01:00
.gitignore Initial document generation support. 2019-01-21 16:57:04 +00:00
Assert.thy Port to Isabelle 2019. 2019-06-23 00:15:50 +01:00
Code_Reflection.thy Initial commit: SML Code Reflection 2019-08-15 20:48:07 +01:00
Hiding_Type_Variables.thy Port to Isabelle 2019. 2019-06-23 00:15:50 +01:00
LICENSE Initial commit. 2018-06-14 19:22:45 +01:00
Nano_JSON.thy Fixed serializer for definitions using equality from Pure. 2019-01-24 23:20:56 +00:00
README.md Initial commit: SML Code Reflection 2019-08-15 20:48:07 +01:00
ROOT Initial commit: SML Code Reflection 2019-08-15 20:48:07 +01:00
example.json Added parser and overall cleanup. 2019-01-21 09:49:22 +00:00

README.md

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 2019, 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.

Authors

Main author: Achim D. Brucker

License

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.