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 6eb7d1cde3 Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 5 months ago
.woodpecker Added email notification for failed builds. 5 months ago
Simple_Oracle/bin Initial commit: example of a simple external oracle. 5 months ago
document Upgrading to Isabelle 2020. 1 year ago
fxp Changed ref to Unsynchronized.ref. 1 year ago
ml-yacc-lib Initial commit: ml-yacc support for Isabelle. 1 year ago
.gitignore Initial document generation support. 4 years ago
Assert.thy Port to Isabelle 2019. 3 years ago
Code_Reflection.thy Initial commit: SML Code Reflection 3 years ago
Fxp.thy Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 5 months ago
Hiding_Type_Variables.thy Port to Isabelle 2019. 3 years ago
LICENSE Initial commit. 4 years ago
Ml_Yacc_Lib.thy Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 5 months ago
Nano_JSON.thy Fixed serializer for definitions using equality from Pure. 4 years ago
README.md Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 5 months ago
ROOT Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 5 months ago
Simple_Oracle.thy Initial commit: example of a simple external oracle. 5 months ago
example.json Added parser and overall cleanup. 4 years ago

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 2021-1, 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.

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

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

  • 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.

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

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

  • Simple_Oracle.thy provides an example on integrating an external tool as simple oracle or counter example generator, similar to the built-in quickcheck.

Authors

Main author: Achim D. Brucker

License

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

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

Upstream Repository

The upstream git repository, i.e., the single source of truth, for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/adbrucker/isabelle-hacks.