2018-06-14 18:22:45 +00:00
|
|
|
# Isabelle Hacks
|
|
|
|
|
|
2018-06-16 22:57:35 +00:00
|
|
|
This project contains small Isabelle "hacks" that provide additional
|
2018-06-17 20:33:19 +00:00
|
|
|
functionality to [Isabelle](https://isabelle.in.tum.de) or showcase
|
2018-06-16 22:57:35 +00:00
|
|
|
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
|
2022-10-29 20:08:03 +00:00
|
|
|
release of Isabelle (Isabelle 2022, at time of writing), hacks for
|
2018-06-16 22:57:35 +00:00
|
|
|
older versions might be available on a dedicated branch.
|
|
|
|
|
|
|
|
|
|
## List of Isabelle Hacks
|
|
|
|
|
|
2018-06-18 08:50:22 +00:00
|
|
|
* [Assert.thy](Assert.thy) provides a new top level command **assert**
|
2018-06-17 20:33:19 +00:00
|
|
|
that provides a simple way for specifying assertions that Isabelle
|
2018-06-16 22:57:35 +00:00
|
|
|
checks while processing a theory.
|
2018-06-14 18:22:45 +00:00
|
|
|
|
2022-04-02 12:12:59 +00:00
|
|
|
* [Code_Reflection.thy](Code_Reflection.thy) provides a new top-level
|
|
|
|
|
command for reflecting generated SML code into Isabelle's ML
|
|
|
|
|
environment.
|
|
|
|
|
|
|
|
|
|
* [Fxp.thy](Fxp.thy) provides Isabelle support for The Functional XML
|
|
|
|
|
Parser (fxp).
|
|
|
|
|
|
2018-06-18 08:50:22 +00:00
|
|
|
* [Hiding_Type_Variables.thy](Hiding_Type_Variables.thy) provides
|
2018-06-17 20:38:59 +00:00
|
|
|
print a setup for defining default type variables of type
|
|
|
|
|
constructors. The default type variables can be hidden in output,
|
2018-06-20 09:57:09 +00:00
|
|
|
e.g., `('a, 'b, 'c) foo` is shown as `(_) foo`. This shorthand
|
2018-06-17 20:38:59 +00:00
|
|
|
notation can also be used in input (using a parse translation),
|
|
|
|
|
which (sometimes) helps to focus on the important parts of complex
|
|
|
|
|
type declarations.
|
|
|
|
|
|
2022-04-02 12:12:59 +00:00
|
|
|
* [Ml_Yacc_Lib.thy](Ml_Yacc_Lib.thy) provides Isabelle support for parser
|
2021-04-28 09:00:12 +00:00
|
|
|
generated by ml-yacc (part of sml/NJ).
|
|
|
|
|
|
2022-03-21 06:50:23 +00:00
|
|
|
* [Simple_Oracle.thy](Simple_Oracle.thy) provides an example on integrating
|
|
|
|
|
an external tool as simple oracle or counter example generator, similar
|
|
|
|
|
to the built-in quickcheck.
|
|
|
|
|
|
2022-10-29 19:36:43 +00:00
|
|
|
### 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](https://www.isa-afp.org/entries/Nano_JSON.html)",
|
|
|
|
|
which contains documentation and examples for using JSON encoded data with
|
|
|
|
|
Isabelle/HOL and Isabelle/ML.
|
|
|
|
|
|
2022-03-21 06:50:23 +00:00
|
|
|
## Authors
|
|
|
|
|
|
|
|
|
|
Main author: [Achim D. Brucker](http://www.brucker.ch/)
|
|
|
|
|
|
|
|
|
|
## License
|
|
|
|
|
|
|
|
|
|
If not otherwise stated, all hacks are licensed under a 2-clause
|
|
|
|
|
BSD-style license.
|
|
|
|
|
|
2018-06-17 07:38:49 +00:00
|
|
|
## Authors
|
|
|
|
|
|
|
|
|
|
Main author: [Achim D. Brucker](http://www.brucker.ch/)
|
|
|
|
|
|
2018-06-14 18:22:45 +00:00
|
|
|
## License
|
2018-06-26 16:28:21 +00:00
|
|
|
|
2018-06-16 22:57:35 +00:00
|
|
|
If not otherwise stated, all hacks are licensed under a 2-clause
|
|
|
|
|
BSD-style license.
|
2018-06-14 18:22:45 +00:00
|
|
|
|
|
|
|
|
SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
|
|
2022-03-28 06:24:02 +00:00
|
|
|
## Upstream Repository
|
2018-06-16 22:57:35 +00:00
|
|
|
|
2022-03-28 06:24:02 +00:00
|
|
|
The upstream git repository, i.e., the single source of truth, for this project is hosted
|
|
|
|
|
by the [Software Assurance & Security Research Team](https://logicalhacking.com) at
|
2018-06-26 23:40:43 +00:00
|
|
|
<https://git.logicalhacking.com/adbrucker/isabelle-hacks>.
|
