e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederDescription : predefined strings of several Isabelle logics
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian MaederCopyright : (c) Uni Bremen 2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian MaederStability : provisional
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian MaederPortability : portable
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian MaederString constants of Isabelle keywords to be excluded by translations
29a1760d2bf1c27214c6b9d94b5047836cbd0ce3Christian Maederobtained by manually taking @lexicon@ and @consts@ from
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian Maeder@print_syntax(theory "...")@
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian Maeder(initial empty strings omitted)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
95620f46e91947602cb7ea280a502b14b21c135dChristian Maeder-- | convert pasted strings to a relevant set of strings
45ac9c4fc2e4ca01feff3c1426a77cf7e952ef69Christian MaedermkIsaSet :: [String] -> Set.Set String
d979c5692ccc2aba170e11f279a8c82850d6359bChristian MaedermkIsaSet = Set.fromList . concatMap words
29a1760d2bf1c27214c6b9d94b5047836cbd0ce3Christian Maeder{- fewer list elements are better to optimize ("\",\"" -> " ")
5421dfe94879c995076603a87a5699714123660eChristian Maeder but keep all words in case we also want to use symbols
29a1760d2bf1c27214c6b9d94b5047836cbd0ce3Christian Maederdata IsaSets = IsaSets
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder { types :: Set.Set String
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder , consts :: Set.Set String
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederholcfS :: IsaSets
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder types = mkIsaSet
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder [ "lBool intT integerT charT ratT lString"
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder , "unitT lOrdering sOrdering llist lprod lEither lMaybe"],
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder consts = mkIsaSet [
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "! !! # $ % & ( () (: (] (| (} ) * **",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "+ ++ , - --> -> -` . .. ... ..} / // 0 1 :",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder ":) :: := ; < <*> <*lex*> <+> << <<| <= <| = ==",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "==> => > >. ? ?! @ ALL BIT CHR EX EX! GREATEST",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "INF INT If Int LAM LEAST LUB Let MOST O OFCLASS",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "PROP SIGMA SOME THE TYPE UN Un WRT [ [\\<mapsto>] []",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "[| [|->] \\<And> \\<Colon> \\<Inter> \\<Inter>\\<^bsub>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<Lambda> \\<Longrightarrow> \\<Prod> \\<Rightarrow> \\<Sigma>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<Squnion> \\<Sum> \\<Union> \\<Union>\\<^bsub> \\<^esub>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<^sub> \\<^sub>1 \\<^sup>* \\<^sup>+ \\<^sup>= \\<and>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<bar> \\<bottom> \\<cdot> \\<circ> \\<dots> \\<epsilon>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<equiv> \\<equiv>\\<^sup>? \\<exists> \\<exists>!",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<exists>\\<^sub>\\<infinity> \\<forall>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<forall>\\<^sub>\\<infinity> \\<in> \\<index> \\<int>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<inter> \\<inverse> \\<lambda> \\<lbrakk> \\<le> \\<leadsto>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<lfloor> \\<longrightarrow> \\<lparr> \\<mapsto>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<mapsto>\\<lambda> \\<nat> \\<not> \\<noteq> \\<notin>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<oplus> \\<or> \\<otimes> \\<rbrakk> \\<rightarrow>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<rightharpoonup> \\<rparr> \\<sqsubseteq> \\<struct>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<subset> \\<subseteq> \\<subseteq>\\<^sub>m \\<times>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<twosuperior> \\<union> ] ^ ^* ^+ ^-1 ^= _ _:: `",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "`> `` andalso case choose div dvd else fi if in",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "let mem mod o of oo op orelse then { {) {..",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "{\\<mapsto>} {|->} {} | |) |-> |] |_ } ~ ~: ~=",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "!! #prop * ** + ++ -> 0 1 == ==> =?=",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@Coll @Finset @INTER @INTER1 @INTER_le @INTER_less @LUB",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@SetCompr @Sigma @Times @UNION @UNION1 @UNION_le @UNION_less",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@andalso @chg_map @cifte @ctuple @filter @list @oo @orelse",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@stuple ACe ALL Abs_CFun Abs_Integ Abs_Nat Abs_Node",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Abs_Prod Abs_Sprod Abs_Ssum Abs_Sum Abs_Up Abs_bin Abs_char",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Abs_discr Abs_lift Abs_list Abs_nibble Abs_option Abs_sumbool",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Abs_unit All Alm_all Atom Ball Bex Bit CFun CLet Case",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Char Cletbind Cletbinds Collect Cons Def Discr Domain",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "EX EX! Eps Ex Ex1 FF False Field Finites GREATEST ",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Goal Greatest GreatestM ID INF INTER Icifte Id If If2",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Ifix Ifup Image In0 In1 Inf_many Inl Inl_Rep Inr",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Inr_Rep Integ Inter Ints Inv Isfst Isinl Isinr Ispair",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Issnd Istrictify Iup Iwhen LAM LC LEAST LUB Leaf",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Least LeastM Left Let Lim MOST Max Min NCons Nat",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Nats Nibble0 Nibble1 Nibble2 Nibble3 Nibble4 Nibble5",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Nibble6 Nibble7 Nibble8 Nibble9 NibbleA NibbleB NibbleC",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "NibbleD NibbleE NibbleF Nil Node None Not Numb Numeral0",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Numeral1 ONE Pair Pair_Rep Part Pls Plus Pow Prod Push",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Push_Node Range Rep_CFun Rep_Integ Rep_Nat Rep_Node Rep_Prod",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Rep_Sprod Rep_Ssum Rep_Sum Rep_Up Rep_bin Rep_char Rep_discr",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Rep_lift Rep_list Rep_nibble Rep_option Rep_sumbool Rep_unit",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Right Scons Sigma Sinl_Rep Sinr_Rep Some Spair_Rep Split",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Sprod Ssum Suc Suc_Rep Sum Suml Summation Sumr TT TYPE",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "The True Trueprop UNION UNIV UU Undef Union Unity Up",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Zero_Rep _Ball _Bex _CLet _Cbind _Cbinds _Char _DDDOT",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_Eps _GreatestM _K _LAM _LUpdate _LeastM _Let _Map",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_MapUpd _Maplets _Numeral _String _Summation _TYPE _The",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_Update _abs _appl _applC _aprop _args _asms _bigimpl",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_bind _binds _bracket _cargs _case1 _case2 _case_syntax",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_classes _constify _constrain _dummy_ofsort _field _field_type",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_field_types _fields _idts _idtyp _index _index1 _indexvar",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_lambda _leAll _leEx _lessAll _lessEx _lupdbind _lupdbinds",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_maplet _maplets _meta_conjunction _mk_ofclass _noindex",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_not_equal _ofclass _ofsort _pattern _patterns _pttrns",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_record _record_scheme _record_type _record_type_scheme",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_record_update _reflcl _setle _setless _setprod _setsum",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_sort _square _struct _tapp _tappl _topsort _tuple",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_tuple_arg _tuple_args _types _update _update_name _updates",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_updbind _updbinds abelian_group abelian_group_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "abelian_semigroup abelian_semigroup_class abs acyclic adjust",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "adm adm_wf admw all almost_ordered_semiring",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "almost_ordered_semiring_class almost_semiring almost_semiring_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "antisym any apfst aprop arbitrary args asms atLeast",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "atLeastAtMost atLeastLessThan atMost atmost_one bij bin",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bin_add bin_case bin_minus bin_mult bin_pred bin_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bin_rec_set bin_rep_set bin_succ binomial bool bool_case",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bool_rec bool_rec_set butlast card cardR cargs case_syn",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "cases_syn cfcomp cfst chain char char_case char_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "char_rec_set char_rep_set chfin chfin_class chg_map classes",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "comp concat congruent congruent2 cont contents contlub",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "converse cpair cpo cpo_class csnd csplit curry cut diag",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "discr discr_case discr_rec discr_rec_set discr_rep_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "distinct div divAlg div_class divide division_by_zero",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "division_by_zero_class dom dprod drop dropWhile dsum dtree",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "dummy dummy_pattern empty equiv even even_odd even_odd_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "field field_class field_type field_types fields filter",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "finite finite_chain finite_class finite_psubset fix flat",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "flat_class flift1 flift2 fold foldSet foldl foldr fst",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "fun fun_upd fup gfp greaterThan greaterThanAtMost",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "greaterThanLessThan hd id ident idt idts image ind index",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "induct_conj induct_equal induct_forall induct_implies infinite",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "inj inj_on insert int int_aux internal_split intrel inv",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "inv_image inverse inverse_class iszero item iterate itself",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "last length lessThan less_cfun less_than letbind letbinds",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "lex lex_prod lexico lexn lfp lift lift_case lift_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "lift_rec_set liftpair linorder linorder_class list list_all",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "list_all2 list_case list_rec list_rec_set list_rep_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "list_update lists logic logic_class longid lub lupdbind",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "lupdbinds map map_add map_image map_le map_of map_subst",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "map_upd_s map_upds maplet maplets max max_in_chain measure",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "min minus minus_class mono monofun myinv nat nat_aux",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "nat_case nat_rec nat_rec_set ndepth neg negDivAlg negateSnd",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "nibble nibble_case nibble_rec nibble_rec_set nibble_rep_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "node nth ntrunc null num num_const number number_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "number_of number_ring number_ring_class o2s odd of_int",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "of_nat one one_class op & op * op + op - op --> op :",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "op < op << op <<| op <= op <| op = op @ op Int op Un",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "op div op dvd op mem op mod op | op ~: option option_case",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "option_map option_rec option_rec_set option_rep_set ord",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ord_class order order_class ordered_field ordered_field_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ordered_ring ordered_ring_class ordered_semiring",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ordered_semiring_class overwrite patterns pcpo pcpo_class plus",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "plus_ac0 plus_ac0_class plus_class po po_class posDivAlg",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "power power_class pred_nat prod_case prod_fun prod_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "prod_rec_set product_type prop pttrn pttrns quorem quotient",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ran range refl reflexive rel_comp remdups replicate",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "restrict_map rev ring ring_class ringpower ringpower_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "rtrancl same_fst semiring semiring_class set setprod setsum",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sfst single_valued sinl sinr size snd sort spair split",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sq_ord sq_ord_class sscase ssnd ssplit strictify string",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "struct sublist sum_case sum_rec sum_rec_set sumbool",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sumbool_case sumbool_rec sumbool_rec_set sumbool_rep_set surj",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sym take takeWhile the tid times times_ac1 times_ac1_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "times_class tl tord tr trancl trand trans tror",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "tuple_args tvar type type_class type_definition types u",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "uminus undiscr unit unit_case unit_rec unit_rec_set up",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "upd_fst upd_snd update updates updbind updbinds uprod upt",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "upto usum var vimage wellorder wellorder_class wf wfrec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "wfrec_rel xnum xstr zero zero_class zip {} ~=>"
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedermainS :: IsaSets
80f5899bc42f833b3ed367d63d6151fa7e3c5ccbChristian Maeder types = mkIsaSet
4cf7d0dab6145fd018a01c6a0519d12a047b4029Christian Maeder ["bool Nat Int int partial list unit char rat string option either *"],
8e4e4d95c7e8591ab44b6edd686694a641350236Christian Maeder consts = mkIsaSet ["2 3 4 5 6 7 8 9",
8e4e4d95c7e8591ab44b6edd686694a641350236Christian Maeder "inject n [__] [__/__] __[__/__] {__} >= > /",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "! !! # % & ( () (] (| (} ) * + ++ ,",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "- --> -` . .. ... ..} / // 0 1 : :: := ; <",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "<*> <*lex*> <+> <= = == ==> => ? ?! @ ALL BIT",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "CHR EX EX! GREATEST INF INT Int LEAST MOST O OFCLASS",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "PROP SIGMA SOME THE TYPE UN Un WRT [ [\\<mapsto>] []",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "[| [|->] \\<And> \\<Colon> \\<Inter> \\<Inter>\\<^bsub>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<Longrightarrow> \\<Prod> \\<Rightarrow> \\<Sigma> \\<Sum>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<Union> \\<Union>\\<^bsub> \\<^esub> \\<^sub> \\<^sub>1",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<^sup>* \\<^sup>+ \\<^sup>= \\<and> \\<bar> \\<circ>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<dots> \\<epsilon> \\<equiv> \\<equiv>\\<^sup>? \\<exists>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<exists>! \\<exists>\\<^sub>\\<infinity> \\<forall>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<forall>\\<^sub>\\<infinity> \\<in> \\<index> \\<int>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<inter> \\<inverse> \\<lambda> \\<lbrakk> \\<le> \\<leadsto>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<lfloor> \\<longrightarrow> \\<lparr> \\<mapsto>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<mapsto>\\<lambda> \\<nat> \\<not> \\<noteq> \\<notin>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<or> \\<rbrakk> \\<rightharpoonup> \\<rparr> \\<struct>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<subset> \\<subseteq> \\<subseteq>\\<^sub>m \\<times>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "\\<twosuperior> \\<union> ] ^ ^* ^+ ^-1 ^= _ _:: `",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "`> `` case choose div dvd else if in let mem mod",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "o of op then { {) {.. {\\<mapsto>} {|->} {} | |)",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "|-> |] |_ } ~ ~: ~= ~=> ~>",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "!! #prop * + 0 1 == ==> =?= @Coll @Finset",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@INTER @INTER1 @INTER_le @INTER_less @SetCompr @Sigma @Times",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "@UNION @UNION1 @UNION_le @UNION_less @chg_map @filter @list",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ACe ALL Abs_Integ Abs_Nat Abs_Node Abs_Prod Abs_Sum",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Abs_bin Abs_char Abs_list Abs_nibble Abs_option Abs_sumbool",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Abs_unit All Alm_all Atom Ball Bex Bit Case Char",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Collect Cons Domain EX EX! Eps Ex Ex1 False Field",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Finites GREATEST Goal Greatest GreatestM INF INTER Id",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "If Image In0 In1 Inf_many Inl Inl_Rep Inr Inr_Rep",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Integ Inter Ints Inv LC LEAST Leaf Least LeastM Left",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Let Lim MOST Max Min NCons Nat Nats Nibble0 Nibble1",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Nibble2 Nibble3 Nibble4 Nibble5 Nibble6 Nibble7 Nibble8",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Nibble9 NibbleA NibbleB NibbleC NibbleD NibbleE NibbleF",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Nil Node None Not Numb Numeral0 Numeral1 Pair Pair_Rep",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Part Pls Plus Pow Prod Push Push_Node Range Rep_Integ",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Rep_Nat Rep_Node Rep_Prod Rep_Sum Rep_bin Rep_char Rep_list",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Rep_nibble Rep_option Rep_sumbool Rep_unit Right Scons Sigma",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "Some Split Suc Suc_Rep Sum Suml Summation Sumr TYPE",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "The True Trueprop UNION UNIV Union Unity Zero_Rep _Ball",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_Bex _Char _DDDOT _Eps _GreatestM _K _LUpdate _LeastM",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_Let _Map _MapUpd _Maplets _Numeral _String _Summation",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_TYPE _The _Update _abs _appl _applC _aprop _args _asms",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_bigimpl _bind _binds _bracket _cargs _case1 _case2",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_case_syntax _classes _constify _constrain _dummy_ofsort",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_field _field_type _field_types _fields _idts _idtyp _index",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_index1 _indexvar _lambda _leAll _leEx _lessAll _lessEx",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_lupdbind _lupdbinds _maplet _maplets _meta_conjunction",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_mk_ofclass _noindex _not_equal _ofclass _ofsort _pattern",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_patterns _pttrns _record _record_scheme _record_type",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_record_type_scheme _record_update _reflcl _setle _setless",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_setprod _setsum _sort _square _struct _tapp _tappl",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_topsort _tuple _tuple_arg _tuple_args _types _update",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "_update_name _updates _updbind _updbinds abelian_group",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "abelian_group_class abelian_semigroup abelian_semigroup_class abs",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "acyclic adjust adm_wf all almost_ordered_semiring",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "almost_ordered_semiring_class almost_semiring almost_semiring_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "antisym any apfst aprop arbitrary args asms atLeast",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "atLeastAtMost atLeastLessThan atMost atmost_one bij bin",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bin_add bin_case bin_minus bin_mult bin_pred bin_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bin_rec_set bin_rep_set bin_succ binomial bool bool_case",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "bool_rec bool_rec_set butlast card cardR cargs case_syn",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "cases_syn char char_case char_rec char_rec_set char_rep_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "chg_map classes comp concat congruent congruent2 contents",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "converse curry cut diag distinct div divAlg div_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "divide division_by_zero division_by_zero_class dom dprod drop",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "dropWhile dsum dtree dummy dummy_pattern empty equiv even",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "even_odd even_odd_class field field_class field_type",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "field_types fields filter finite finite_class finite_psubset",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "fold foldSet foldl foldr fst fun fun_upd gfp greaterThan",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "greaterThanAtMost greaterThanLessThan hd id ident idt idts",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "image ind index induct_conj induct_equal induct_forall",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "induct_implies infinite inj inj_on insert int int_aux",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "internal_split intrel inv inv_image inverse inverse_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "iszero item itself last length lessThan less_than letbind",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "letbinds lex lex_prod lexico lexn lfp linorder",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "linorder_class list list_all list_all2 list_case list_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "list_rec_set list_rep_set list_update lists logic logic_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "longid lupdbind lupdbinds map map_add map_image map_le",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "map_of map_subst map_upd_s map_upds maplet maplets max",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "measure min minus minus_class mono myinv nat nat_aux",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "nat_case nat_rec nat_rec_set ndepth neg negDivAlg negateSnd",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "nibble nibble_case nibble_rec nibble_rec_set nibble_rep_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "node nth ntrunc null num num_const number number_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "number_of number_ring number_ring_class o2s odd of_int",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "of_nat one one_class op & op * op + op - op --> op :",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "op < op <= op = op @ op Int op Un op div op dvd op mem",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "op mod op | op ~: option option_case option_map option_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "option_rec_set option_rep_set ord ord_class order order_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ordered_field ordered_field_class ordered_ring ordered_ring_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ordered_semiring ordered_semiring_class overwrite patterns plus",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "plus_ac0 plus_ac0_class plus_class posDivAlg power power_class",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "pred_nat prod_case prod_fun prod_rec prod_rec_set product_type",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "prop pttrn pttrns quorem quotient ran range refl",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "reflexive rel_comp remdups replicate restrict_map rev ring",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "ring_class ringpower ringpower_class rtrancl same_fst semiring",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "semiring_class set setprod setsum single_valued size snd",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sort split string struct sublist sum_case sum_rec",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sum_rec_set sumbool sumbool_case sumbool_rec sumbool_rec_set",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "sumbool_rep_set surj sym take takeWhile the tid times",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "times_ac1 times_ac1_class times_class tl trancl trans",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "tuple_args tvar type type_class type_definition types uminus",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "unit unit_case unit_rec unit_rec_set upd_fst upd_snd update",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "updates updbind updbinds uprod upt upto usum var vimage",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "wellorder wellorder_class wf wfrec wfrec_rel xnum xstr",
d979c5692ccc2aba170e11f279a8c82850d6359bChristian Maeder "zero zero_class zip {} ~=>"