1structure temporalSyntax :> temporalSyntax = 2struct 3 4open Abbrev HolKernel progSyntax temporalTheory 5 6val ERR = Feedback.mk_HOL_ERR "tripleSyntax" 7 8(* ----------------------------------------------------------------------- *) 9 10fun syntax_fns n d m = 11 HolKernel.syntax_fns {n = n, dest = d, make = m} "temporal" 12 13val s1 = syntax_fns 3 HolKernel.dest_monop HolKernel.mk_monop 14val s2 = syntax_fns 4 HolKernel.dest_binop HolKernel.mk_binop 15 16val (temporal_tm, mk_temporal, dest_temporal, is_temporal) = 17 HolKernel.syntax_fns3 "temporal" "TEMPORAL" 18val (now_tm, mk_now, dest_now, is_now) = s1 "NOW" 19val (next_tm, mk_next, dest_next, is_next) = s1 "NEXT" 20val (eventually_tm, mk_eventually, dest_eventually, is_eventually) = 21 s1 "EVENTUALLY" 22val (always_tm, mk_always, dest_always, is_always) = s1 "ALWAYS" 23val (t_and_tm, mk_t_and, dest_t_and, is_t_and) = s2 "T_AND" 24val (t_implies_tm, mk_t_implies, dest_t_implies, is_t_implies) = s2 "T_IMPLIES" 25 26(* ----------------------------------------------------------------------- *) 27 28end 29