History log of /seL4-l4v-master/l4v/lib/FP_Eval.thy
Revision Date Author Comments
# a45adef6 31-Oct-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

all: remove theory import path references

In Isabelle2020, when isabelle jedit is started without a session
context, e.g. `isabelle jedit -l ASpec`, theory imports with path
references cause the isabelle process to hang.

Since sessions now declare directories, Isabelle can find those files
without path reference and we therefore remove all such path references
from import statements. With this, `jedit` and `build` should work with
and without explicit session context as before.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>


# a424d55e 09-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX


# 9cbf5e6a 10-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: use `@{term_pat}` in FP_Eval; refactor term_pat testsuite


# 4c18e1f1 09-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib/FP_Eval: add license headers


# c94d3285 09-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib/FP_Eval: move let_weak_cong' to main tool; improve docs


# 450f83ff 08-Apr-2019 Japheth Lim <Japheth.Lim@data61.csiro.au>

lib: initial version of FP_Eval tool

FP_Eval is an Isabelle/ML tool for functional program rewriting.
It has similarities with the Isabelle simplifier, but is simpler and
more scalable for performing computations in the logic.

See FP_Eval_Tests for basic tests and examples.