History log of /seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ltlScript.sml
Revision Date Author Comments
# da23fd3f 22-Apr-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

LTL example: use zDefine for derived syntax to stop EVAL expanding

In particular, stop expansion of F_TRUE, LTL_F and LTL_G.


# 9b2e7e11 24-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

added some example formulae


# 15e945ce 05-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on d_conj_set lemm for concrete gba


# cdb07a19 20-Sep-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on correctness for concrete ltl -> waa


# 2acb56a7 15-Sep-2017 Simon Jantsch <simon.jantsch@gmail.com>

strict TSF is WF


# 49b1da5a 27-Aug-2017 Simon Jantsch <simon.jantsch@gmail.com>

added support for full ltl formulae


# 4c732463 27-Aug-2017 Simon Jantsch <simon.jantsch@gmail.com>

renamed example directory and added it to tools/sequences/final-examples