{- |

Module : $Header$

Copyright : (c) Uni Bremen 2005

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : portable

String constants of Isabelle keywords to be excluded by translations

obtained by manually taking @lexicon@ and @consts@ from

@print_syntax(theory "...")@

(initial empty strings omitted)

-}

module Isabelle.IsaStrings where

import qualified Common.Lib.Set as Set

import Data.Char

isIsaChar :: Char -> Bool

isIsaChar c = isAlphaNum c && isAscii c || c `elem` "_'"

mkIsaSet :: [String] -> Set.Set String

mkIsaSet =

foldr ( \ s -> if all isIsaChar s then Set.insert s else id) Set.empty

pureS :: Set.Set String

pureS = mkIsaSet [

"!!","%","(",")",",",".","...","::",";","==","==>","=>","OFCLASS",

"PROP","TYPE","[","[|","\\<And>","\\<Colon>","\\<Longrightarrow>",

"\\<Rightarrow>","\\<^sub>","\\<dots>","\\<equiv>","\\<equiv>\\<^sup>?",

"\\<index>","\\<lambda>","\\<lbrakk>","\\<rbrakk>","\\<struct>","]","_",

"_::","op","{","{}","|]","}",

"!!","!!","#prop","==","==","==>","==>","==>","=?=","Goal",

"Goal","TYPE","_DDDOT","_DDDOT","_K","_TYPE","_abs","_appl","_appl",

"_aprop","_args","_asms","_bigimpl","_bigimpl","_bracket","_bracket",

"_classes","_constify","_constrain","_constrain","_dummy_ofsort","_idts",

"_idtyp","_idtyp","_index","_indexvar","_lambda","_lambda",

"_meta_conjunction","_mk_ofclass","_noindex","_ofclass","_ofsort",

"_ofsort","_pttrns","_sort","_struct","_tapp","_tappl","_topsort","_types",

"all","any","aprop","args","asms","cargs","classes","dummy","dummy",

"dummy_pattern","dummy_pattern","fun","fun","fun","id","idt","idts",

"index","itself","logic","logic","logic_class","longid","num","num_const",

"prop","pttrn","pttrns","sort","struct","tid","tvar","type","types","var",

"xnum","xstr"

]

holS :: Set.Set String

holS = mkIsaSet [

"!","!!","%","&","(",")","*","+",",","-","-->",".","...","/","0",

"1","::",";","<","<=","=","==","==>","=>","?","?!","ALL","EX","EX!",

"LEAST","OFCLASS","PROP","THE","TYPE","[","[|","\\<And>","\\<Colon>",

"\\<Longrightarrow>","\\<Rightarrow>","\\<^sub>","\\<^sub>1","\\<and>",

"\\<bar>","\\<dots>","\\<equiv>","\\<equiv>\\<^sup>?","\\<exists>",

"\\<exists>!","\\<forall>","\\<index>","\\<lambda>","\\<lbrakk>","\\<le>",

"\\<longrightarrow>","\\<not>","\\<noteq>","\\<or>","\\<rbrakk>",

"\\<struct>","]","_","_::","case","else","if","in","let","of","op","then",

"{","{}","|","|]","}","~","~=",

"!!","!!","#prop","0","1","==","==","==>","==>","==>",

"=?=","ALL ","ALL ","ALL ","ALL ","All","EX ","EX ","EX ","EX ","EX! ",

"EX! ","EX! ","EX! ","Ex","Ex1","False","Goal","Goal","If","LEAST ",

"Least","Let","Not","Not","Not","TYPE","The","True","Trueprop","_DDDOT",

"_DDDOT","_K","_Let","_TYPE","_The","_abs","_appl","_applC","_aprop",

"_args","_asms","_bigimpl","_bigimpl","_bind","_binds","_bracket",

"_bracket","_cargs","_case1","_case1","_case2","_case_syntax","_classes",

"_constify","_constrain","_constrain","_dummy_ofsort","_idts","_idtyp",

"_idtyp","_index","_index1","_indexvar","_lambda","_lambda","_leAll",

"_leAll","_leAll","_leAll","_leEx","_leEx","_leEx","_leEx","_lessAll",

"_lessAll","_lessAll","_lessAll","_lessEx","_lessEx","_lessEx","_lessEx",

"_meta_conjunction","_mk_ofclass","_noindex","_not_equal","_not_equal",

"_not_equal","_not_equal","_not_equal","_ofclass","_ofsort","_ofsort",

"_pttrns","_sort","_struct","_tapp","_tappl","_topsort","_types","abs",

"abs","abs","all","any","aprop","arbitrary","args","asms","bool","cargs",

"case_syn","cases_syn","classes","divide","dummy","dummy","dummy_pattern",

"dummy_pattern","fun","fun","fun","id","idt","idts","index","induct_conj",

"induct_equal","induct_forall","induct_implies","inverse","inverse",

"inverse_class","itself","letbind","letbinds","linorder","linorder_class",

"logic","logic","logic_class","longid","max","min","minus","minus_class",

"mono","num","num_const","one","one_class","op &","op &","op &","op *",

"op +","op -","op -->","op -->","op <","op <","op <=","op <=","op <=",

"op <=","op =","op =","op |","op |","op |","ord","ord_class","order",

"order_class","plus","plus_class","prop","pttrn","pttrns","sort","struct",

"tid","times","times_class","tvar","type","type","type_class","types",

"uminus","var","xnum","xstr","zero","zero_class"

]

holcfS :: Set.Set String

holcfS = mkIsaSet [

"!","!!","#","$","%","&","(","()","(:","(]","(|","(}",")","*","**",

"+","++",",","-","-->","->","-`",".","..","...","..}","/","//","0","1",":",

":)","::",":=",";","<","<*>","<*lex*>","<+>","<<","<<|","<=","<|","=","==",

"==>","=>",">",">.","?","?!","@","ALL","BIT","CHR","EX","EX!","GREATEST",

"INF","INT","If","Int","LAM","LEAST","LUB","Let","MOST","O","OFCLASS",

"PROP","SIGMA","SOME","THE","TYPE","UN","Un","WRT","[","[\\<mapsto>]","[]",

"[|","[|->]","\\<And>","\\<Colon>","\\<Inter>","\\<Inter>\\<^bsub>",

"\\<Lambda>","\\<Longrightarrow>","\\<Prod>","\\<Rightarrow>","\\<Sigma>",

"\\<Squnion>","\\<Sum>","\\<Union>","\\<Union>\\<^bsub>","\\<^esub>",

"\\<^sub>","\\<^sub>1","\\<^sup>*","\\<^sup>+","\\<^sup>=","\\<and>",

"\\<bar>","\\<bottom>","\\<cdot>","\\<circ>","\\<dots>","\\<epsilon>",

"\\<equiv>","\\<equiv>\\<^sup>?","\\<exists>","\\<exists>!",

"\\<exists>\\<^sub>\\<infinity>","\\<forall>",

"\\<forall>\\<^sub>\\<infinity>","\\<in>","\\<index>","\\<int>",

"\\<inter>","\\<inverse>","\\<lambda>","\\<lbrakk>","\\<le>","\\<leadsto>",

"\\<lfloor>","\\<longrightarrow>","\\<lparr>","\\<mapsto>",

"\\<mapsto>\\<lambda>","\\<nat>","\\<not>","\\<noteq>","\\<notin>",

"\\<oplus>","\\<or>","\\<otimes>","\\<rbrakk>","\\<rightarrow>",

"\\<rightharpoonup>","\\<rparr>","\\<sqsubseteq>","\\<struct>",

"\\<subset>","\\<subseteq>","\\<subseteq>\\<^sub>m","\\<times>",

"\\<twosuperior>","\\<union>","]","^","^*","^+","^-1","^=","_","_::","`",

"`>","``","andalso","case","choose","div","dvd","else","fi","if","in",

"let","mem","mod","o","of","oo","op","orelse","then","{","{)","{..",

"{\\<mapsto>}","{|->}","{}","|","|)","|->","|]","|_","}","~","~:","~=",

"~=>","~>",

"!!","#prop","*","**","+","++","->","0","1","==","==>","=?=",

"@Coll","@Finset","@INTER","@INTER1","@INTER_le","@INTER_less","@LUB",

"@SetCompr","@Sigma","@Times","@UNION","@UNION1","@UNION_le","@UNION_less",

"@andalso","@chg_map","@cifte","@ctuple","@filter","@list","@oo","@orelse",

"@stuple","ACe","ALL ","Abs_CFun","Abs_Integ","Abs_Nat","Abs_Node",

"Abs_Prod","Abs_Sprod","Abs_Ssum","Abs_Sum","Abs_Up","Abs_bin","Abs_char",

"Abs_discr","Abs_lift","Abs_list","Abs_nibble","Abs_option","Abs_sumbool",

"Abs_unit","All","Alm_all","Atom","Ball","Bex","Bit","CFun","CLet","Case",

"Char","Cletbind","Cletbinds","Collect","Cons","Def","Discr","Domain",

"EX ","EX! ","Eps","Ex","Ex1","FF","False","Field","Finites","GREATEST ",

"Goal","Greatest","GreatestM","ID","INF ","INTER","Icifte","Id","If","If2",

"Ifix","Ifup","Image","In0","In1","Inf_many","Inl","Inl_Rep","Inr",

"Inr_Rep","Integ","Inter","Ints","Inv","Isfst","Isinl","Isinr","Ispair",

"Issnd","Istrictify","Iup","Iwhen","LAM ","LC","LEAST ","LUB ","Leaf",

"Least","LeastM","Left","Let","Lim","MOST ","Max","Min","NCons","Nat",

"Nats","Nibble0","Nibble1","Nibble2","Nibble3","Nibble4","Nibble5",

"Nibble6","Nibble7","Nibble8","Nibble9","NibbleA","NibbleB","NibbleC",

"NibbleD","NibbleE","NibbleF","Nil","Node","None","Not","Numb","Numeral0",

"Numeral1","ONE","Pair","Pair_Rep","Part","Pls","Plus","Pow","Prod","Push",

"Push_Node","Range","Rep_CFun","Rep_Integ","Rep_Nat","Rep_Node","Rep_Prod",

"Rep_Sprod","Rep_Ssum","Rep_Sum","Rep_Up","Rep_bin","Rep_char","Rep_discr",

"Rep_lift","Rep_list","Rep_nibble","Rep_option","Rep_sumbool","Rep_unit",

"Right","Scons","Sigma","Sinl_Rep","Sinr_Rep","Some","Spair_Rep","Split",

"Sprod","Ssum","Suc","Suc_Rep","Sum","Suml","Summation","Sumr","TT","TYPE",

"The","True","Trueprop","UNION","UNIV","UU","Undef","Union","Unity","Up",

"Zero_Rep","_Ball","_Bex","_CLet","_Cbind","_Cbinds","_Char","_DDDOT",

"_Eps","_GreatestM","_K","_LAM","_LUpdate","_LeastM","_Let","_Map",

"_MapUpd","_Maplets","_Numeral","_String","_Summation","_TYPE","_The",

"_Update","_abs","_appl","_applC","_aprop","_args","_asms","_bigimpl",

"_bind","_binds","_bracket","_cargs","_case1","_case2","_case_syntax",

"_classes","_constify","_constrain","_dummy_ofsort","_field","_field_type",

"_field_types","_fields","_idts","_idtyp","_index","_index1","_indexvar",

"_lambda","_leAll","_leEx","_lessAll","_lessEx","_lupdbind","_lupdbinds",

"_maplet","_maplets","_meta_conjunction","_mk_ofclass","_noindex",

"_not_equal","_ofclass","_ofsort","_pattern","_patterns","_pttrns",

"_record","_record_scheme","_record_type","_record_type_scheme",

"_record_update","_reflcl","_setle","_setless","_setprod","_setsum",

"_sort","_square","_struct","_tapp","_tappl","_topsort","_tuple",

"_tuple_arg","_tuple_args","_types","_update","_update_name","_updates",

"_updbind","_updbinds","abelian_group","abelian_group_class",

"abelian_semigroup","abelian_semigroup_class","abs","acyclic","adjust",

"adm","adm_wf","admw","all","almost_ordered_semiring",

"almost_ordered_semiring_class","almost_semiring","almost_semiring_class",

"antisym","any","apfst","aprop","arbitrary","args","asms","atLeast",

"atLeastAtMost","atLeastLessThan","atMost","atmost_one","bij","bin",

"bin_add","bin_case","bin_minus","bin_mult","bin_pred","bin_rec",

"bin_rec_set","bin_rep_set","bin_succ","binomial","bool","bool_case",

"bool_rec","bool_rec_set","butlast","card","cardR","cargs","case_syn",

"cases_syn","cfcomp","cfst","chain","char","char_case","char_rec",

"char_rec_set","char_rep_set","chfin","chfin_class","chg_map","classes",

"comp","concat","congruent","congruent2","cont","contents","contlub",

"converse","cpair","cpo","cpo_class","csnd","csplit","curry","cut","diag",

"discr","discr_case","discr_rec","discr_rec_set","discr_rep_set",

"distinct","div","divAlg","div_class","divide","division_by_zero",

"division_by_zero_class","dom","dprod","drop","dropWhile","dsum","dtree",

"dummy","dummy_pattern","empty","equiv","even","even_odd","even_odd_class",

"field","field_class","field_type","field_types","fields","filter",

"finite","finite_chain","finite_class","finite_psubset","fix","flat",

"flat_class","flift1","flift2","fold","foldSet","foldl","foldr","fst",

"fun","fun_upd","fup","gfp","greaterThan","greaterThanAtMost",

"greaterThanLessThan","hd","id","ident","idt","idts","image","ind","index",

"induct_conj","induct_equal","induct_forall","induct_implies","infinite",

"inj","inj_on","insert","int","int_aux","internal_split","intrel","inv",

"inv_image","inverse","inverse_class","iszero","item","iterate","itself",

"last","length","lessThan","less_cfun","less_than","letbind","letbinds",

"lex","lex_prod","lexico","lexn","lfp","lift","lift_case","lift_rec",

"lift_rec_set","liftpair","linorder","linorder_class","list","list_all",

"list_all2","list_case","list_rec","list_rec_set","list_rep_set",

"list_update","lists","logic","logic_class","longid","lub","lupdbind",

"lupdbinds","map","map_add","map_image","map_le","map_of","map_subst",

"map_upd_s","map_upds","maplet","maplets","max","max_in_chain","measure",

"min","minus","minus_class","mono","monofun","myinv","nat","nat_aux",

"nat_case","nat_rec","nat_rec_set","ndepth","neg","negDivAlg","negateSnd",

"nibble","nibble_case","nibble_rec","nibble_rec_set","nibble_rep_set",

"node","nth","ntrunc","null","num","num_const","number","number_class",

"number_of","number_ring","number_ring_class","o2s","odd","of_int",

"of_nat","one","one_class","op &","op *","op +","op -","op -->","op :",

"op <","op <<","op <<|","op <=","op <|","op =","op @","op Int","op Un",

"op div","op dvd","op mem","op mod","op |","op ~:","option","option_case",

"option_map","option_rec","option_rec_set","option_rep_set","ord",

"ord_class","order","order_class","ordered_field","ordered_field_class",

"ordered_ring","ordered_ring_class","ordered_semiring",

"ordered_semiring_class","overwrite","patterns","pcpo","pcpo_class","plus",

"plus_ac0","plus_ac0_class","plus_class","po","po_class","posDivAlg",

"power","power_class","pred_nat","prod_case","prod_fun","prod_rec",

"prod_rec_set","product_type","prop","pttrn","pttrns","quorem","quotient",

"ran","range","refl","reflexive","rel_comp","remdups","replicate",

"restrict_map","rev","ring","ring_class","ringpower","ringpower_class",

"rtrancl","same_fst","semiring","semiring_class","set","setprod","setsum",

"sfst","single_valued","sinl","sinr","size","snd","sort","spair","split",

"sq_ord","sq_ord_class","sscase","ssnd","ssplit","strictify","string",

"struct","sublist","sum_case","sum_rec","sum_rec_set","sumbool",

"sumbool_case","sumbool_rec","sumbool_rec_set","sumbool_rep_set","surj",

"sym","take","takeWhile","the","tid","times","times_ac1","times_ac1_class",

"times_class","tl","tord","tr","trancl","trand","trans","tror",

"tuple_args","tvar","type","type_class","type_definition","types","u",

"uminus","undiscr","unit","unit_case","unit_rec","unit_rec_set","up",

"upd_fst","upd_snd","update","updates","updbind","updbinds","uprod","upt",

"upto","usum","var","vimage","wellorder","wellorder_class","wf","wfrec",

"wfrec_rel","xnum","xstr","zero","zero_class","zip","{}","~=>"

]

mainS :: Set.Set String

mainS = mkIsaSet [

"!","!!","#","%","&","(","()","(]","(|","(}",")","*","+","++",",",

"-","-->","-`",".","..","...","..}","/","//","0","1",":","::",":=",";","<",

"<*>","<*lex*>","<+>","<=","=","==","==>","=>","?","?!","@","ALL","BIT",

"CHR","EX","EX!","GREATEST","INF","INT","Int","LEAST","MOST","O","OFCLASS",

"PROP","SIGMA","SOME","THE","TYPE","UN","Un","WRT","[","[\\<mapsto>]","[]",

"[|","[|->]","\\<And>","\\<Colon>","\\<Inter>","\\<Inter>\\<^bsub>",

"\\<Longrightarrow>","\\<Prod>","\\<Rightarrow>","\\<Sigma>","\\<Sum>",

"\\<Union>","\\<Union>\\<^bsub>","\\<^esub>","\\<^sub>","\\<^sub>1",

"\\<^sup>*","\\<^sup>+","\\<^sup>=","\\<and>","\\<bar>","\\<circ>",

"\\<dots>","\\<epsilon>","\\<equiv>","\\<equiv>\\<^sup>?","\\<exists>",

"\\<exists>!","\\<exists>\\<^sub>\\<infinity>","\\<forall>",

"\\<forall>\\<^sub>\\<infinity>","\\<in>","\\<index>","\\<int>",

"\\<inter>","\\<inverse>","\\<lambda>","\\<lbrakk>","\\<le>","\\<leadsto>",

"\\<lfloor>","\\<longrightarrow>","\\<lparr>","\\<mapsto>",

"\\<mapsto>\\<lambda>","\\<nat>","\\<not>","\\<noteq>","\\<notin>",

"\\<or>","\\<rbrakk>","\\<rightharpoonup>","\\<rparr>","\\<struct>",

"\\<subset>","\\<subseteq>","\\<subseteq>\\<^sub>m","\\<times>",

"\\<twosuperior>","\\<union>","]","^","^*","^+","^-1","^=","_","_::","`",

"`>","``","case","choose","div","dvd","else","if","in","let","mem","mod",

"o","of","op","then","{","{)","{..","{\\<mapsto>}","{|->}","{}","|","|)",

"|->","|]","|_","}","~","~:","~=","~=>","~>",

"!!","#prop","*","+","0","1","==","==>","=?=","@Coll","@Finset",

"@INTER","@INTER1","@INTER_le","@INTER_less","@SetCompr","@Sigma","@Times",

"@UNION","@UNION1","@UNION_le","@UNION_less","@chg_map","@filter","@list",

"ACe","ALL ","Abs_Integ","Abs_Nat","Abs_Node","Abs_Prod","Abs_Sum",

"Abs_bin","Abs_char","Abs_list","Abs_nibble","Abs_option","Abs_sumbool",

"Abs_unit","All","Alm_all","Atom","Ball","Bex","Bit","Case","Char",

"Collect","Cons","Domain","EX ","EX! ","Eps","Ex","Ex1","False","Field",

"Finites","GREATEST ","Goal","Greatest","GreatestM","INF ","INTER","Id",

"If","Image","In0","In1","Inf_many","Inl","Inl_Rep","Inr","Inr_Rep",

"Integ","Inter","Ints","Inv","LC","LEAST ","Leaf","Least","LeastM","Left",

"Let","Lim","MOST ","Max","Min","NCons","Nat","Nats","Nibble0","Nibble1",

"Nibble2","Nibble3","Nibble4","Nibble5","Nibble6","Nibble7","Nibble8",

"Nibble9","NibbleA","NibbleB","NibbleC","NibbleD","NibbleE","NibbleF",

"Nil","Node","None","Not","Numb","Numeral0","Numeral1","Pair","Pair_Rep",

"Part","Pls","Plus","Pow","Prod","Push","Push_Node","Range","Rep_Integ",

"Rep_Nat","Rep_Node","Rep_Prod","Rep_Sum","Rep_bin","Rep_char","Rep_list",

"Rep_nibble","Rep_option","Rep_sumbool","Rep_unit","Right","Scons","Sigma",

"Some","Split","Suc","Suc_Rep","Sum","Suml","Summation","Sumr","TYPE",

"The","True","Trueprop","UNION","UNIV","Union","Unity","Zero_Rep","_Ball",

"_Bex","_Char","_DDDOT","_Eps","_GreatestM","_K","_LUpdate","_LeastM",

"_Let","_Map","_MapUpd","_Maplets","_Numeral","_String","_Summation",

"_TYPE","_The","_Update","_abs","_appl","_applC","_aprop","_args","_asms",

"_bigimpl","_bind","_binds","_bracket","_cargs","_case1","_case2",

"_case_syntax","_classes","_constify","_constrain","_dummy_ofsort",

"_field","_field_type","_field_types","_fields","_idts","_idtyp","_index",

"_index1","_indexvar","_lambda","_leAll","_leEx","_lessAll","_lessEx",

"_lupdbind","_lupdbinds","_maplet","_maplets","_meta_conjunction",

"_mk_ofclass","_noindex","_not_equal","_ofclass","_ofsort","_pattern",

"_patterns","_pttrns","_record","_record_scheme","_record_type",

"_record_type_scheme","_record_update","_reflcl","_setle","_setless",

"_setprod","_setsum","_sort","_square","_struct","_tapp","_tappl",

"_topsort","_tuple","_tuple_arg","_tuple_args","_types","_update",

"_update_name","_updates","_updbind","_updbinds","abelian_group",

"abelian_group_class","abelian_semigroup","abelian_semigroup_class","abs",

"acyclic","adjust","adm_wf","all","almost_ordered_semiring",

"almost_ordered_semiring_class","almost_semiring","almost_semiring_class",

"antisym","any","apfst","aprop","arbitrary","args","asms","atLeast",

"atLeastAtMost","atLeastLessThan","atMost","atmost_one","bij","bin",

"bin_add","bin_case","bin_minus","bin_mult","bin_pred","bin_rec",

"bin_rec_set","bin_rep_set","bin_succ","binomial","bool","bool_case",

"bool_rec","bool_rec_set","butlast","card","cardR","cargs","case_syn",

"cases_syn","char","char_case","char_rec","char_rec_set","char_rep_set",

"chg_map","classes","comp","concat","congruent","congruent2","contents",

"converse","curry","cut","diag","distinct","div","divAlg","div_class",

"divide","division_by_zero","division_by_zero_class","dom","dprod","drop",

"dropWhile","dsum","dtree","dummy","dummy_pattern","empty","equiv","even",

"even_odd","even_odd_class","field","field_class","field_type",

"field_types","fields","filter","finite","finite_class","finite_psubset",

"fold","foldSet","foldl","foldr","fst","fun","fun_upd","gfp","greaterThan",

"greaterThanAtMost","greaterThanLessThan","hd","id","ident","idt","idts",

"image","ind","index","induct_conj","induct_equal","induct_forall",

"induct_implies","infinite","inj","inj_on","insert","int","int_aux",

"internal_split","intrel","inv","inv_image","inverse","inverse_class",

"iszero","item","itself","last","length","lessThan","less_than","letbind",

"letbinds","lex","lex_prod","lexico","lexn","lfp","linorder",

"linorder_class","list","list_all","list_all2","list_case","list_rec",

"list_rec_set","list_rep_set","list_update","lists","logic","logic_class",

"longid","lupdbind","lupdbinds","map","map_add","map_image","map_le",

"map_of","map_subst","map_upd_s","map_upds","maplet","maplets","max",

"measure","min","minus","minus_class","mono","myinv","nat","nat_aux",

"nat_case","nat_rec","nat_rec_set","ndepth","neg","negDivAlg","negateSnd",

"nibble","nibble_case","nibble_rec","nibble_rec_set","nibble_rep_set",

"node","nth","ntrunc","null","num","num_const","number","number_class",

"number_of","number_ring","number_ring_class","o2s","odd","of_int",

"of_nat","one","one_class","op &","op *","op +","op -","op -->","op :",

"op <","op <=","op =","op @","op Int","op Un","op div","op dvd","op mem",

"op mod","op |","op ~:","option","option_case","option_map","option_rec",

"option_rec_set","option_rep_set","ord","ord_class","order","order_class",

"ordered_field","ordered_field_class","ordered_ring","ordered_ring_class",

"ordered_semiring","ordered_semiring_class","overwrite","patterns","plus",

"plus_ac0","plus_ac0_class","plus_class","posDivAlg","power","power_class",

"pred_nat","prod_case","prod_fun","prod_rec","prod_rec_set","product_type",

"prop","pttrn","pttrns","quorem","quotient","ran","range","refl",

"reflexive","rel_comp","remdups","replicate","restrict_map","rev","ring",

"ring_class","ringpower","ringpower_class","rtrancl","same_fst","semiring",

"semiring_class","set","setprod","setsum","single_valued","size","snd",

"sort","split","string","struct","sublist","sum_case","sum_rec",

"sum_rec_set","sumbool","sumbool_case","sumbool_rec","sumbool_rec_set",

"sumbool_rep_set","surj","sym","take","takeWhile","the","tid","times",

"times_ac1","times_ac1_class","times_class","tl","trancl","trans",

"tuple_args","tvar","type","type_class","type_definition","types","uminus",

"unit","unit_case","unit_rec","unit_rec_set","upd_fst","upd_snd","update",

"updates","updbind","updbinds","uprod","upt","upto","usum","var","vimage",

"wellorder","wellorder_class","wf","wfrec","wfrec_rel","xnum","xstr",

"zero","zero_class","zip","{}","~=>"

]