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