1signature GrammarSpecials =
2sig
3
4  val fnapp_special : string
5  val bracket_special : string
6  val vs_cons_special : string
7  val resquan_special : string
8  val let_special : string
9  val letcons_special : string
10  val letnil_special : string
11  val and_special : string
12  val fakeconst_special : string
13  val mk_fakeconst_name :
14      {original : KernelSig.kernelname option, fake : string} -> string
15  val dest_fakeconst_name :
16      string -> {original : KernelSig.kernelname option, fake : string} option
17  val decimal_fraction_special : string
18
19  (* special strings for records *)
20  val recsel_special : string
21  val recupd_special : string
22  val recfupd_special : string
23  val reccons_special : string
24  val recnil_special : string
25  val recwith_special : string
26  val bigrec_subdivider_string : string
27
28  val std_binder_precedence : int
29
30  val nat_elim_term : string
31  val fromNum_str : string
32  val num_injection : string
33  val mk_lform_name : {cons:string,nilstr:string} -> string
34  val term_name_is_lform : string -> bool
35  val recd_lform_name : string
36
37  (* handling case expressions *)
38  val mk_case_special : string -> string
39  val dest_case_special : string -> string option
40  val is_case_special : string -> bool
41  val core_case_special : string
42  val case_split_special : string
43  val case_arrow_special : string
44
45  val set_case_specials :
46      ((Term.term -> Term.term) *
47       ({Thy:string,Tyop:string} -> Term.term list)) -> unit
48  val compile_pattern_match : Term.term -> Term.term
49  val type_constructors : {Thy:string,Tyop:string} -> Term.term list
50  val case_initialised : unit -> bool
51
52
53end
54