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