#
f51c777e |
|
06-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
temporal_deep example: ensure it works with both standard and experimental kernel
|
#
81ba0c9a |
|
05-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
cleanup temporal_deep - replace "ITERATE" with "FUNPOW" - replace "POWER_SET" with "POW" - replace "PRED_SET_FORALL" with "RES_FORALL" - move "POS_START" to translationsLib and plan for later removal - remove various lemmata and use lemmata from standard libs instead - remove Know and Suff
|
#
7d68bd97 |
|
05-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
work on temporal_deep example Following some work by Chun Tian, this commit makes the temporal_deep example compile again. This example got severe bit-rot unluckily. There is still more work to do: - the libraries have not been tested yet - the theories contaimn now many constants and lemmata now present in standard libraries - the proofs are ugly using strange constructs which are hard to maintain (I hope I learned something about HOL within the last 10 years since I created this example) So, this commit is just a first step and more cleanup work will follow.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
1e90d3ff |
|
18-Oct-2006 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Some deep embeddings of temporal logics and some related tools. Especially there are translations between PSL and LTL and between LTL and omega-automata. Additionally, there is an interface to SMV
|