adbrucker/isabelle-hacks
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
A Collection of Isabelle Programming Hacks
83 Commits 1 Branch 6 Tags 426 KiB
Standard ML 82.1%
HTML 10.4%
Isabelle 5.9%
Makefile 0.6%
Scala 0.4%
Other 0.6%
main
Go to file
Achim D. Brucker 840c2d63ed
All checks were successful
ci/woodpecker/push/build Pipeline was successful
Details
Initial commit.
2023-05-14 17:37:28 +02:00
.woodpecker Initial commit. 2023-05-14 17:37:28 +02:00
document Upgrading to Isabelle 2020. 2021-03-06 01:01:08 +00:00
fxp Changed ref to Unsynchronized.ref. 2021-04-28 09:27:40 +01:00
ml-yacc-lib Initial commit: ml-yacc support for Isabelle. 2021-04-28 09:58:18 +01:00
Simple_Oracle/bin Initial commit: example of a simple external oracle. 2022-03-21 06:50:23 +00: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 Tuned. 2023-02-13 07:23:23 +00:00
Fxp.thy Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 2022-04-02 13:12:59 +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
Ml_Yacc_Lib.thy Renaming to comply with the usual naming convention that theory names start with an uppercase letter. 2022-04-02 13:12:59 +01:00
README.md Update to Isabelle 2022. 2022-10-29 21:08:03 +01:00
ROOT Removed Nano_JSON, which is is now an official AFP entry: https://www.isa-afp.org/entries/Nano_JSON.html 2022-10-29 20:36:43 +01:00
Simple_Oracle.thy Initial commit: example of a simple external oracle. 2022-03-21 06:50:23 +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 2022, 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).

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

No Longer Maintained Hacks

  • Nano_JSON.thy (support for a JSON-like data exchange for Isabelle/HOL) has been developed into an AFP entry "Nano_JSON", which contains documentation and examples for using JSON encoded data with Isabelle/HOL and Isabelle/ML.

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.