1" 2" Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3" 4" SPDX-License-Identifier: BSD-2-Clause 5" 6 7" 8" Parts of this file were originally contributed by 9" Jens-Wolfhard Schicke-Uffmann <drahflow@gmx.de> 10" 11 12" 13" Vim syntax highlighting for THY files. 14" 15" This syntax will show UTF-8 Isabelle symbols if you have concealling enabled. 16" If you use this, you will probably want it automatically enabled whenever you 17" open an Isabelle theory. So whenever you detect and enable the syntax, set 18" the conceal level as well: 19" 20" au BufRead,BufNewFile *.thy setfiletype isabelle 21" au BufRead,BufNewFile *.thy set conceallevel=2 22" 23" If you regularly need to toggle this on and off you can bind it to a key: 24" 25" function! ToggleConceal() 26" if &conceallevel == 0 27" set conceallevel=2 28" else 29" set conceallevel=0 30" endif 31" endfunction 32" nm <F6> :call ToggleConceal()<CR> 33" imap <F6> <C-o>:call ToggleConceal()<CR> 34" 35 36syn clear 37syn sync fromstart 38syn case match 39 40syn keyword IsabelleCommand term typ prop prf full_prf pr value 41syn keyword IsabelleCommand abbreviation 42syn keyword IsabelleCommand theory 43syn keyword IsabelleCommand theorem schematic_theorem corollary 44 \ schematic_corollary 45syn keyword IsabelleCommand lemma 46syn keyword IsabelleCommand lemmas 47syn keyword IsabelleCommand schematic_lemma 48syn keyword IsabelleCommand primrec 49syn keyword IsabelleCommand datatype 50syn keyword IsabelleCommand declare declaration syntax_declaration 51syn keyword IsabelleCommand definition 52syn keyword IsabelleCommand fun 53syn keyword IsabelleCommand function termination 54syn keyword IsabelleCommand typedecl 55syn keyword IsabelleCommand types 56syn keyword IsabelleCommand typedef 57syn keyword IsabelleCommand type_synonym 58syn keyword IsabelleCommand consts 59syn keyword IsabelleCommand constdefs 60syn keyword IsabelleCommand inductive 61syn keyword IsabelleCommand inductive_set 62syn keyword IsabelleCommand inductive_cases 63syn keyword IsabelleCommand record 64syn keyword IsabelleCommand defs 65syn keyword IsabelleCommand axclass 66syn keyword IsabelleCommand instance 67syn keyword IsabelleCommand axioms 68syn keyword IsabelleCommand axiomatization 69syn keyword IsabelleCommand locale 70syn keyword IsabelleCommand sublocale 71syn keyword IsabelleCommand theorems 72syn keyword IsabelleCommand class subclass 73syn keyword IsabelleCommand interpretation interpret 74syn keyword IsabelleCommand instantiation 75syn keyword IsabelleCommand context 76syn keyword IsabelleCommand rep_datatype 77syn keyword IsabelleCommand export_code 78syn keyword IsabelleCommand code_const 79syn keyword IsabelleCommand ML_file 80syn keyword IsabelleCommand setup 81syn keyword IsabelleCommand thm find_theorems 82syn keyword IsabelleCommand print_theorems print_locale print_locales 83 \ print_dependencies print_interps print_classes class_deps print_abbrevs 84 \ print_statement print_trans_rules print_cases print_induct_rules 85syn keyword IsabelleCommand notepad 86syn keyword IsabelleCommand nonterminal syntax no_syntax translations 87 \ no_translations 88 89" Do some juggling to give us ML highlighting inside an Isabelle/ML block. 90if exists('b:current_syntax') 91 let s:current_syntax=b:current_syntax 92 unlet b:current_syntax 93endif 94syntax include @SML syntax/sml.vim 95if exists('s:current_syntax') 96 let b:current_syntax=s:current_syntax 97else 98 unlet b:current_syntax 99endif 100syntax region IsabelleCommand matchgroup=SpecialComment fold start="ML\_s*\({\*\|\\<open>\)" end="\(\*}\|\\<close>\)" contains=@SML 101syntax region IsabelleCommand matchgroup=SpecialComment fold start="method_setup\_s*\a\w*\_s*=\_s*\({\*\|\\<open>\)" end="\(\*}\|\\<close>\)\_s*\(\"[^\"]*\"\)\?" contains=@SML 102 103" Excessively complicated way of matching (* ... *) comments to support nested 104" blocks. 105syntax region IsabelleComment matchgroup=IsabelleComment start="(\*" end="\*)" contains=IsabelleCommentStart 106syntax match IsabelleCommentStart "(\*" contained nextgroup=IsabelleCommentContent contains=IsabelleCommentStart 107syntax match IsabelleCommentContent ".*" contained 108 109syntax region IsabelleComment matchgroup=IsabelleComment fold start="\\<comment>\s*\\<open>" end="\\<close>" contains=IsabelleSpecial keepend 110 111" You can use LaTeX within text {* ... *} blocks and friends and sometimes it 112" is useful to have syntax highlighting enabled within these blocks when 113" working on a PDF-destined theory. This is off by default because it can be a 114" little distracting when not working on documentation. You can put something 115" like the following in your ~/.vimrc for easy toggling of LaTeX syntax: 116" 117" function! ToggleIsabelleTex() 118" if exists('g:isabelle_tex') 119" let g:isabelle_tex = !g:isabelle_tex 120" else 121" let g:isabelle_tex=1 122" endif 123" syntax off 124" syntax on 125" endfunction 126" nm <F8> :call ToggleIsabelleTex()<CR> 127" imap <F8> <C-o>:call ToggleIsabelleTex()<CR> 128" 129if exists('g:isabelle_tex') && g:isabelle_tex == 1 130 if exists('b:current_syntax') 131 let s:current_syntax=b:current_syntax 132 unlet b:current_syntax 133 endif 134 syntax include @TEX syntax/tex.vim 135 if exists('s:current_syntax') 136 let b:current_syntax=s:current_syntax 137 else 138 unlet b:current_syntax 139 endif 140 syntax region IsabelleCommand matchgroup=IsabelleComment fold start="\(chapter\|text\|txt\|header\|\(sub\)*section\)[ ]*{\*" end="\*}" contains=@TEX 141 " The TeX syntax meddles with iskeyword and thereby screws up syntax 142 " highlighting for anything involving an underscore after it has been loaded. 143 " Reset this here. 144 set iskeyword+=_ 145else 146 " If g:isabelle_tex is not set, just highlight these blocks as normal 147 " comments. 148 syn match IsabelleComment "\(chapter\|text\|txt\|header\|\(sub\)*section\)[ ]*{\*\_.\{-}\*}" 149endif 150 151syn keyword IsabelleCommandPart and is 152syn keyword IsabelleCommandPart assumes constrains defines shows fixes notes 153 \ obtains 154syn keyword IsabelleCommandPart where for 155syn keyword IsabelleCommandPart begin end 156syn keyword IsabelleCommandPart imports 157syn keyword IsabelleCommandPart keywords uses 158syn keyword IsabelleCommandPart monos overloaded 159syn keyword IsabelleCommandMod code simp iff rule_format cong 160syn match IsabelleCommandMod /\<intro\>!\?/ 161syn match IsabelleCommandMod /\<dest\>!\?/ 162syn keyword IsabelleCommandProofProve proof 163syn keyword IsabelleCommandProofProve apply 164syn keyword IsabelleCommandProofProve prefer defer 165syn keyword IsabelleCommandProofBad back 166syn keyword IsabelleCommandProofDone done by qed apply_end 167syn keyword IsabelleCommandProofFail sorry oops 168syn keyword IsabelleCommandProofIsar assume show have from then thus hence 169 \ presume def 170syn match IsabelleGoalProofIsar /?\<thesis\>/ 171syn match IsabelleGoalProofIsar /?\<case\>/ 172syn keyword IsabelleGoalProofIsar assms 173syn keyword IsabelleCommandProofIsar with next using note 174syn keyword IsabelleCommandProofIsar let 175syn keyword IsabelleCommandProofIsar moreover ultimately also finally 176syn keyword IsabelleCommandProofIsar fix obtain where case guess 177syn keyword IsabelleCommandMethod assumption fact this 178syn keyword IsabelleCommandMethod rule erule drule frule 179syn keyword IsabelleCommandMethod elim 180syn match IsabelleCommandMethod /\<intro\>/ 181syn keyword IsabelleCommandMethod intro_classes intro_locales 182syn keyword IsabelleCommandMethod rule_tac erule_tac drule_tac frule_tac 183syn keyword IsabelleCommandMethod insert subst hypsubst 184syn keyword IsabelleCommandMethod rename_tac rotate_tac 185syn keyword IsabelleCommandMethod induct_tac ind_cases induct 186syn keyword IsabelleCommandMethod coinduct 187syn keyword IsabelleCommandMethod induct_scheme lexicographic_order relation 188syn keyword IsabelleCommandMethod case_tac cases split 189syn keyword IsabelleCommandMethod subgoal_tac 190syn keyword IsabelleCommandMethod eval evaluation 191syn keyword IsabelleCommandMethod fail succeed 192syn keyword IsabelleCommandMethod atomize atomize_elim 193syn keyword IsabelleCommandMethod neg_clausify finish_clausify 194syn keyword IsabelleCommandMethod contradiction 195syn keyword IsabelleCommandMethod cut_tac 196syn keyword IsabelleCommandMethod fold unfold unfold_locales unfolding 197syn keyword IsabelleCommandMethod normalization sring_norm 198syn match IsabelleCommandMethodMod /\<add!\?:/ 199syn match IsabelleCommandMethodMod /\<del!\?:/ 200syn match IsabelleCommandMethodMod /\<only!\?:/ 201syn match IsabelleCommandMethodMod /\<dest!\?:/ 202syn match IsabelleCommandMethodMod /\<intro!\?:/ 203syn match IsabelleCommandMethodMod /\<split!\?:/ 204syn match IsabelleCommandMethodMod /\<cong!\?:/ 205syn match IsabelleCommandMethodMod /\<arbitrary!\?:/ 206syn keyword IsabelleCommandMethodMod in no_asm_use 207syn keyword IsabelleCommandMethodMod thin_tac 208syn keyword IsabelleCommandBigMethod simp simp_all 209syn keyword IsabelleCommandBigMethod blast force auto fast best slow deepen fastforce 210syn keyword IsabelleCommandBigMethod unat_arith arith algebra 211syn keyword IsabelleCommandBigMethod bestsimp fastsimp simplesubst slowsimp 212syn keyword IsabelleCommandBigMethod clarify safe clarsimp default 213syn keyword IsabelleCommandBigMethod eprover eproverF eproverH 214syn keyword IsabelleCommandBigMethod iprover 215syn keyword IsabelleCommandBigMethod metis metisF metisH 216syn keyword IsabelleCommandBigMethod meson order pat_completeness 217syn keyword IsabelleCommandBigMethod presburger 218syn keyword IsabelleCommandBigMethod rtrancl rtranclp trancl tranclp 219syn keyword IsabelleCommandBigMethod sat satx 220syn keyword IsabelleCommandBigMethod spass spassF spassH 221syn keyword IsabelleCommandBigMethod tactic raw_tactic 222syn keyword IsabelleCommandBigMethod vampire vampireF vampireH 223syn keyword IsabelleCommandRule conjI conjE conjunct1 conjunct2 224syn keyword IsabelleCommandRule disjI1 disjI2 disjE disjCI 225syn keyword IsabelleCommandRule notI notE 226syn keyword IsabelleCommandRule impI 227syn keyword IsabelleCommandRule mp 228syn keyword IsabelleCommandRule ssubst subst 229syn keyword IsabelleCommandRule contrapos_np contrapos_nn 230syn keyword IsabelleCommandRule contrapos_pp contrapos_pn 231syn keyword IsabelleCommandRule allI allE spec 232syn keyword IsabelleCommandRule exI exE 233syn keyword IsabelleCommandRule the_equality 234syn keyword IsabelleCommandRule some_equality someI someI2 someI_ex 235syn keyword IsabelleCommandRule order_antisym 236syn keyword IsabelleCommandRule sym 237syn keyword IsabelleCommandRule iffD1 iffD2 238syn keyword IsabelleCommandRule arg_cong 239syn keyword IsabelleCommandRule mult_le_mono1 240syn keyword IsabelleCommandRule mod_Suc 241syn keyword IsabelleCommandRule mod_div_equality 242syn keyword IsabelleCommandRule dvd_mod_imp_dvd dvd_mod dvd_trans 243syn keyword IsabelleCommandRule IntI IntD1 IntD2 244syn keyword IsabelleCommandRule Compl_iff Compl_Un Compl_partition 245syn keyword IsabelleCommandRule Diff_disjoint 246syn keyword IsabelleCommandRule subsetI subsetD 247syn keyword IsabelleCommandRule Un_subset_iff 248syn keyword IsabelleCommandRule set_ext 249syn keyword IsabelleCommandRule equalityI equalityE 250syn keyword IsabelleCommandRule insert_is_Un 251syn keyword IsabelleCommandRule mem_Collect_eq Collect_mem_eq 252syn keyword IsabelleCommandRule ballI bspec bexI bexE 253syn keyword IsabelleCommandRule UN_iff UN_I UN_E Union_iff 254syn keyword IsabelleCommandRule INT_iff Inter_iff 255syn keyword IsabelleCommandRule card_Un_Int card_Pow 256syn keyword IsabelleCommandRule n_subsets 257syn keyword IsabelleCommandRule ext id_def o_def o_assoc 258syn keyword IsabelleCommandRule fun_upd_apply fun_upd_upd 259syn keyword IsabelleCommandRule inj_on_def surj_def bij_def 260syn keyword IsabelleCommandRule inv_f_f surj_f_inv_f inv_inv_eq 261syn keyword IsabelleCommandRule expand_fun_eq 262syn keyword IsabelleCommandRule image_def image_compose image_Un image_Int 263syn keyword IsabelleCommandRule vimage_def vimage_Compl 264syn keyword IsabelleCommandRule Id_def rel_comp_def R_O_Id rel_comp_mono 265syn keyword IsabelleCommandRule converse_iff Image_iff Domain_iff Range_iff 266syn keyword IsabelleCommandRule rtrancl_unfold rtrancl_refl 267syn keyword IsabelleCommandRule r_into_rtrancl rtrancl_trans 268syn keyword IsabelleCommandRule rtrancl_induct rtrancl_idemp 269syn keyword IsabelleCommandRule converse_rtrancl_induct 270syn keyword IsabelleCommandRule trancl_trans trancl_converse 271syn keyword IsabelleCommandRule less_than_iff wf_less_than 272syn keyword IsabelleCommandRule inv_image_def wf_inv_image 273syn keyword IsabelleCommandRule measure_def wf_measure 274syn keyword IsabelleCommandRule lex_prod_def wf_lex_prod 275syn keyword IsabelleCommandRule wf_induct 276syn keyword IsabelleCommandRule mono_def monoI monoD 277syn keyword IsabelleCommandRule lfp_unfold lfp_induct lfp_induct_set 278syn keyword IsabelleCommandRule lfp_lowerbound 279syn keyword IsabelleCommandRule gfp_unfold coinduct 280syn keyword IsabelleCommandRuleMod asm of OF THEN simplified where symmetric 281 \ standard 282syn match IsabelleCommandRule /\<[a-zA-Z][a-zA-Z0-9_']*_def\>/ 283syn match IsabelleCommandPart /|/ 284 285syn region IsabelleInner matchgroup=IsabelleInnerMarker start=+"+ end=+"+ contains=@IsabelleInnerStuff 286 287syn match IsabelleSpecial /\\<lambda>\|%/ 288syn match IsabelleSpecial /\\<circ>\|\<o\>/ 289syn match IsabelleSpecial /\<O\>/ 290syn match IsabelleSpecial /\./ 291 292" Collapse Isabelle escape sequences. 293syn match IsabelleSpecial /\\<supseteq>/ conceal cchar=��� 294syn match IsabelleSpecial /\\<KK>/ conceal cchar=���� 295syn match IsabelleSpecial /\\<up>/ conceal cchar=��� 296syn match IsabelleSpecial /\\<otimes>/ conceal cchar=��� 297syn match IsabelleSpecial /\\<aa>/ conceal cchar=���� 298syn match IsabelleSpecial /\\<dagger>/ conceal cchar=��� 299syn match IsabelleSpecial /\\<frown>/ conceal cchar=��� 300syn match IsabelleSpecial /\\<guillemotleft>/ conceal cchar=�� 301syn match IsabelleSpecial /\\<qq>/ conceal cchar=���� 302syn match IsabelleSpecial /\\<X>/ conceal cchar=���� 303syn match IsabelleSpecial /\\<triangleright>/ conceal cchar=��� 304syn match IsabelleSpecial /\\<guillemotright>/ conceal cchar=�� 305syn match IsabelleSpecial /\\<nu>/ conceal cchar=�� 306syn match IsabelleSpecial /\\<sim>/ conceal cchar=��� 307syn match IsabelleSpecial /\\<rightharpoondown>/ conceal cchar=��� 308syn match IsabelleSpecial /\\<p>/ conceal cchar=���� 309syn match IsabelleSpecial /\\<Up>/ conceal cchar=��� 310syn match IsabelleSpecial /\\<triangleq>/ conceal cchar=��� 311syn match IsabelleSpecial /\\<nine>/ conceal cchar=���� 312syn match IsabelleSpecial /\\<preceq>/ conceal cchar=��� 313syn match IsabelleSpecial /\\<nabla>/ conceal cchar=��� 314syn match IsabelleSpecial /\\<FF>/ conceal cchar=���� 315syn match IsabelleSpecial /\\<Im>/ conceal cchar=��� 316syn match IsabelleSpecial /\\<VV>/ conceal cchar=���� 317syn match IsabelleSpecial /\\<spacespace>/ conceal cchar=��� 318syn match IsabelleSpecial /\\<and>/ conceal cchar=��� 319syn match IsabelleSpecial /\\<mapsto>/ conceal cchar=��� 320syn match IsabelleSpecial /\\<ll>/ conceal cchar=���� 321syn match IsabelleSpecial /\\<F>/ conceal cchar=��� 322syn match IsabelleSpecial /\\<degree>/ conceal cchar=�� 323syn match IsabelleSpecial /\\<beta>/ conceal cchar=�� 324syn match IsabelleSpecial /\\<Colon>/ conceal cchar=��� 325syn match IsabelleSpecial /\\<bool>/ conceal cchar=���� 326syn match IsabelleSpecial /\\<e>/ conceal cchar=���� 327syn match IsabelleSpecial /\\<lozenge>/ conceal cchar=��� 328syn match IsabelleSpecial /\\<u>/ conceal cchar=���� 329syn match IsabelleSpecial /\\<sharp>/ conceal cchar=��� 330syn match IsabelleSpecial /\\<Longleftrightarrow>/ conceal cchar=��� 331syn match IsabelleSpecial /\\<Otimes>/ conceal cchar=��� 332syn match IsabelleSpecial /\\<EE>/ conceal cchar=���� 333syn match IsabelleSpecial /\\<I>/ conceal cchar=��� 334syn match IsabelleSpecial /\\<UU>/ conceal cchar=���� 335syn match IsabelleSpecial /\\<exclamdown>/ conceal cchar=�� 336syn match IsabelleSpecial /\\<dots>/ conceal cchar=��� 337syn match IsabelleSpecial /\\<N>/ conceal cchar=���� 338syn match IsabelleSpecial /\\<kk>/ conceal cchar=���� 339syn match IsabelleSpecial /\\<plusminus>/ conceal cchar=�� 340syn match IsabelleSpecial /\\<E>/ conceal cchar=��� 341syn match IsabelleSpecial /\\<triangle>/ conceal cchar=��� 342syn match IsabelleSpecial /\\<eta>/ conceal cchar=�� 343syn match IsabelleSpecial /\\<triangleleft>/ conceal cchar=��� 344syn match IsabelleSpecial /\\<chi>/ conceal cchar=�� 345syn match IsabelleSpecial /\\<z>/ conceal cchar=���� 346syn match IsabelleSpecial /\\<hungarumlaut>/ conceal cchar=�� 347syn match IsabelleSpecial /\\<partial>/ conceal cchar=��� 348syn match IsabelleSpecial /\\<three>/ conceal cchar=���� 349syn match IsabelleSpecial /\\<lesssim>/ conceal cchar=��� 350syn match IsabelleSpecial /\\<subset>/ conceal cchar=��� 351syn match IsabelleSpecial /\\<H>/ conceal cchar=��� 352syn match IsabelleSpecial /\\<leftarrow>/ conceal cchar=��� 353syn match IsabelleSpecial /\\<PP>/ conceal cchar=���� 354syn match IsabelleSpecial /\\<sqsupseteq>/ conceal cchar=��� 355syn match IsabelleSpecial /\\<R>/ conceal cchar=��� 356syn match IsabelleSpecial /\\<bowtie>/ conceal cchar=��� 357syn match IsabelleSpecial /\\<C>/ conceal cchar=���� 358syn match IsabelleSpecial /\\<ddagger>/ conceal cchar=��� 359syn match IsabelleSpecial /\\<ff>/ conceal cchar=���� 360syn match IsabelleSpecial /\\<turnstile>/ conceal cchar=��� 361syn match IsabelleSpecial /\\<bar>/ conceal cchar=�� 362syn match IsabelleSpecial /\\<propto>/ conceal cchar=��� 363syn match IsabelleSpecial /\\<S>/ conceal cchar=���� 364syn match IsabelleSpecial /\\<vv>/ conceal cchar=���� 365syn match IsabelleSpecial /\\<lhd>/ conceal cchar=��� 366syn match IsabelleSpecial /\\<paragraph>/ conceal cchar=�� 367syn match IsabelleSpecial /\\<mu>/ conceal cchar=�� 368syn match IsabelleSpecial /\\<rightharpoonup>/ conceal cchar=��� 369syn match IsabelleSpecial /\\<Inter>/ conceal cchar=��� 370syn match IsabelleSpecial /\\<o>/ conceal cchar=���� 371syn match IsabelleSpecial /\\<asymp>/ conceal cchar=��� 372syn match IsabelleSpecial /\\<Leftarrow>/ conceal cchar=��� 373syn match IsabelleSpecial /\\<Sqinter>/ conceal cchar=��� 374syn match IsabelleSpecial /\\<eight>/ conceal cchar=���� 375syn match IsabelleSpecial /\\<succeq>/ conceal cchar=��� 376syn match IsabelleSpecial /\\<forall>/ conceal cchar=��� 377syn match IsabelleSpecial /\\<complex>/ conceal cchar=��� 378syn match IsabelleSpecial /\\<GG>/ conceal cchar=���� 379syn match IsabelleSpecial /\\<Coprod>/ conceal cchar=��� 380syn match IsabelleSpecial /\\<L>/ conceal cchar=��� 381syn match IsabelleSpecial /\\<WW>/ conceal cchar=���� 382syn match IsabelleSpecial /\\<leadsto>/ conceal cchar=��� 383syn match IsabelleSpecial /\\<D>/ conceal cchar=���� 384syn match IsabelleSpecial /\\<angle>/ conceal cchar=��� 385syn match IsabelleSpecial /\\<section>/ conceal cchar=�� 386syn match IsabelleSpecial /\\<TTurnstile>/ conceal cchar=��� 387syn match IsabelleSpecial /\\<mm>/ conceal cchar=���� 388syn match IsabelleSpecial /\\<T>/ conceal cchar=���� 389syn match IsabelleSpecial /\\<alpha>/ conceal cchar=�� 390syn match IsabelleSpecial /\\<leftharpoondown>/ conceal cchar=��� 391syn match IsabelleSpecial /\\<rho>/ conceal cchar=�� 392syn match IsabelleSpecial /\\<wrong>/ conceal cchar=��� 393syn match IsabelleSpecial /\\<l>/ conceal cchar=���� 394syn match IsabelleSpecial /\\<doteq>/ conceal cchar=��� 395syn match IsabelleSpecial /\\<times>/ conceal cchar=�� 396syn match IsabelleSpecial /\\<noteq>/ conceal cchar=��� 397syn match IsabelleSpecial /\\<rangle>/ conceal cchar=��� 398syn match IsabelleSpecial /\\<div>/ conceal cchar=�� 399syn match IsabelleSpecial /\\<Longrightarrow>/ conceal cchar=��� 400syn match IsabelleSpecial /\\<BB>/ conceal cchar=���� 401syn match IsabelleSpecial /\\<sqsupset>/ conceal cchar=��� 402syn match IsabelleSpecial /\\<rightarrow>/ conceal cchar=��� 403syn match IsabelleSpecial /\\<real>/ conceal cchar=��� 404syn match IsabelleSpecial /\\<hh>/ conceal cchar=���� 405syn match IsabelleSpecial /\\<Phi>/ conceal cchar=�� 406syn match IsabelleSpecial /\\<integral>/ conceal cchar=��� 407syn match IsabelleSpecial /\\<CC>/ conceal cchar=��� 408syn match IsabelleSpecial /\\<euro>/ conceal cchar=��� 409syn match IsabelleSpecial /\\<xx>/ conceal cchar=���� 410syn match IsabelleSpecial /\\<Y>/ conceal cchar=���� 411syn match IsabelleSpecial /\\<zeta>/ conceal cchar=�� 412syn match IsabelleSpecial /\\<longleftarrow>/ conceal cchar=��� 413syn match IsabelleSpecial /\\<a>/ conceal cchar=���� 414syn match IsabelleSpecial /\\<onequarter>/ conceal cchar=�� 415syn match IsabelleSpecial /\\<And>/ conceal cchar=��� 416syn match IsabelleSpecial /\\<downharpoonright>/ conceal cchar=��� 417syn match IsabelleSpecial /\\<phi>/ conceal cchar=�� 418syn match IsabelleSpecial /\\<q>/ conceal cchar=���� 419syn match IsabelleSpecial /\\<Rightarrow>/ conceal cchar=��� 420syn match IsabelleSpecial /\\<clubsuit>/ conceal cchar=��� 421syn match IsabelleSpecial /\\<ggreater>/ conceal cchar=��� 422syn match IsabelleSpecial /\\<two>/ conceal cchar=���� 423syn match IsabelleSpecial /\\<succ>/ conceal cchar=��� 424syn match IsabelleSpecial /\\<AA>/ conceal cchar=���� 425syn match IsabelleSpecial /\\<lparr>/ conceal cchar=��� 426syn match IsabelleSpecial /\\<Squnion>/ conceal cchar=��� 427syn match IsabelleSpecial /\\<HH>/ conceal cchar=��� 428syn match IsabelleSpecial /\\<sqsubseteq>/ conceal cchar=��� 429syn match IsabelleSpecial /\\<QQ>/ conceal cchar=���� 430syn match IsabelleSpecial /\\<setminus>/ conceal cchar=��� 431syn match IsabelleSpecial /\\<Lambda>/ conceal cchar=�� 432syn match IsabelleSpecial /\\<Re>/ conceal cchar=��� 433syn match IsabelleSpecial /\\<J>/ conceal cchar=���� 434syn match IsabelleSpecial /\\<gg>/ conceal cchar=���� 435syn match IsabelleSpecial /\\<hyphen>/ conceal cchar=�� 436syn match IsabelleSpecial /\\<B>/ conceal cchar=��� 437syn match IsabelleSpecial /\\<Z>/ conceal cchar=���� 438syn match IsabelleSpecial /\\<ww>/ conceal cchar=���� 439syn match IsabelleSpecial /\\<lambda>/ conceal cchar=�� 440syn match IsabelleSpecial /\\<onehalf>/ conceal cchar=�� 441syn match IsabelleSpecial /\\<f>/ conceal cchar=���� 442syn match IsabelleSpecial /\\<Or>/ conceal cchar=��� 443syn match IsabelleSpecial /\\<v>/ conceal cchar=���� 444syn match IsabelleSpecial /\\<natural>/ conceal cchar=��� 445syn match IsabelleSpecial /\\<seven>/ conceal cchar=���� 446syn match IsabelleSpecial /\\<Oplus>/ conceal cchar=��� 447syn match IsabelleSpecial /\\<subseteq>/ conceal cchar=��� 448syn match IsabelleSpecial /\\<rfloor>/ conceal cchar=��� 449syn match IsabelleSpecial /\\<LL>/ conceal cchar=���� 450syn match IsabelleSpecial /\\<Sum>/ conceal cchar=��� 451syn match IsabelleSpecial /\\<ominus>/ conceal cchar=��� 452syn match IsabelleSpecial /\\<bb>/ conceal cchar=���� 453syn match IsabelleSpecial /\\<Pi>/ conceal cchar=�� 454syn match IsabelleSpecial /\\<cent>/ conceal cchar=�� 455syn match IsabelleSpecial /\\<diamond>/ conceal cchar=��� 456syn match IsabelleSpecial /\\<mho>/ conceal cchar=��� 457syn match IsabelleSpecial /\\<O>/ conceal cchar=���� 458syn match IsabelleSpecial /\\<rr>/ conceal cchar=���� 459syn match IsabelleSpecial /\\<twosuperior>/ conceal cchar=�� 460syn match IsabelleSpecial /\\<leftharpoonup>/ conceal cchar=��� 461syn match IsabelleSpecial /\\<pi>/ conceal cchar=�� 462syn match IsabelleSpecial /\\<k>/ conceal cchar=���� 463syn match IsabelleSpecial /\\<star>/ conceal cchar=��� 464syn match IsabelleSpecial /\\<rightleftharpoons>/ conceal cchar=��� 465syn match IsabelleSpecial /\\<equiv>/ conceal cchar=��� 466syn match IsabelleSpecial /\\<langle>/ conceal cchar=��� 467syn match IsabelleSpecial /\\<Longleftarrow>/ conceal cchar=��� 468syn match IsabelleSpecial /\\<nexists>/ conceal cchar=��� 469syn match IsabelleSpecial /\\<Odot>/ conceal cchar=��� 470syn match IsabelleSpecial /\\<lfloor>/ conceal cchar=��� 471syn match IsabelleSpecial /\\<sqsubset>/ conceal cchar=��� 472syn match IsabelleSpecial /\\<SS>/ conceal cchar=���� 473syn match IsabelleSpecial /\\<box>/ conceal cchar=��� 474syn match IsabelleSpecial /\\<index>/ conceal cchar=�� 475syn match IsabelleSpecial /\\<pounds>/ conceal cchar=�� 476syn match IsabelleSpecial /\\<Upsilon>/ conceal cchar=�� 477syn match IsabelleSpecial /\\<ii>/ conceal cchar=���� 478syn match IsabelleSpecial /\\<hookleftarrow>/ conceal cchar=��� 479syn match IsabelleSpecial /\\<P>/ conceal cchar=���� 480syn match IsabelleSpecial /\\<threesuperior>/ conceal cchar=�� 481syn match IsabelleSpecial /\\<epsilon>/ conceal cchar=�� 482syn match IsabelleSpecial /\\<yy>/ conceal cchar=���� 483syn match IsabelleSpecial /\\<h>/ conceal cchar=���� 484syn match IsabelleSpecial /\\<upsilon>/ conceal cchar=�� 485syn match IsabelleSpecial /\\<x>/ conceal cchar=���� 486syn match IsabelleSpecial /\\<not>/ conceal cchar=�� 487syn match IsabelleSpecial /\\<le>/ conceal cchar=��� 488syn match IsabelleSpecial /\\<one>/ conceal cchar=���� 489syn match IsabelleSpecial /\\<cdots>/ conceal cchar=��� 490syn match IsabelleSpecial /\\<some>/ conceal cchar=�� 491syn match IsabelleSpecial /\\<Prod>/ conceal cchar=��� 492syn match IsabelleSpecial /\\<NN>/ conceal cchar=���� 493syn match IsabelleSpecial /\\<squnion>/ conceal cchar=��� 494syn match IsabelleSpecial /\\<dd>/ conceal cchar=���� 495syn match IsabelleSpecial /\\<top>/ conceal cchar=��� 496syn match IsabelleSpecial /\\<dieresis>/ conceal cchar=�� 497syn match IsabelleSpecial /\\<tt>/ conceal cchar=���� 498syn match IsabelleSpecial /\\<U>/ conceal cchar=���� 499syn match IsabelleSpecial /\\<unlhd>/ conceal cchar=��� 500syn match IsabelleSpecial /\\<cedilla>/ conceal cchar=�� 501syn match IsabelleSpecial /\\<kappa>/ conceal cchar=�� 502syn match IsabelleSpecial /\\<amalg>/ conceal cchar=��� 503syn match IsabelleSpecial /\\<restriction>/ conceal cchar=��� 504syn match IsabelleSpecial /\\<struct>/ conceal cchar=��� 505syn match IsabelleSpecial /\\<m>/ conceal cchar=���� 506syn match IsabelleSpecial /\\<six>/ conceal cchar=���� 507syn match IsabelleSpecial /\\<midarrow>/ conceal cchar=��� 508syn match IsabelleSpecial /\\<lbrace>/ conceal cchar=��� 509syn match IsabelleSpecial /\\<lessapprox>/ conceal cchar=��� 510syn match IsabelleSpecial /\\<MM>/ conceal cchar=���� 511syn match IsabelleSpecial /\\<down>/ conceal cchar=��� 512syn match IsabelleSpecial /\\<oplus>/ conceal cchar=��� 513syn match IsabelleSpecial /\\<wp>/ conceal cchar=��� 514syn match IsabelleSpecial /\\<surd>/ conceal cchar=��� 515syn match IsabelleSpecial /\\<cc>/ conceal cchar=���� 516syn match IsabelleSpecial /\\<bottom>/ conceal cchar=��� 517syn match IsabelleSpecial /\\<copyright>/ conceal cchar=�� 518syn match IsabelleSpecial /\\<ZZ>/ conceal cchar=��� 519syn match IsabelleSpecial /\\<union>/ conceal cchar=��� 520syn match IsabelleSpecial /\\<V>/ conceal cchar=���� 521syn match IsabelleSpecial /\\<ss>/ conceal cchar=���� 522syn match IsabelleSpecial /\\<unrhd>/ conceal cchar=��� 523syn match IsabelleSpecial /\\<onesuperior>/ conceal cchar=�� 524syn match IsabelleSpecial /\\<b>/ conceal cchar=���� 525syn match IsabelleSpecial /\\<downharpoonleft>/ conceal cchar=��� 526syn match IsabelleSpecial /\\<cdot>/ conceal cchar=��� 527syn match IsabelleSpecial /\\<r>/ conceal cchar=���� 528syn match IsabelleSpecial /\\<Midarrow>/ conceal cchar=��� 529syn match IsabelleSpecial /\\<Down>/ conceal cchar=��� 530syn match IsabelleSpecial /\\<diamondsuit>/ conceal cchar=��� 531syn match IsabelleSpecial /\\<rbrakk>/ conceal cchar=��� 532syn match IsabelleSpecial /\\<lless>/ conceal cchar=��� 533syn match IsabelleSpecial /\\<longleftrightarrow>/ conceal cchar=��� 534syn match IsabelleSpecial /\\<prec>/ conceal cchar=��� 535syn match IsabelleSpecial /\\<emptyset>/ conceal cchar=��� 536syn match IsabelleSpecial /\\<rparr>/ conceal cchar=��� 537syn match IsabelleSpecial /\\<Delta>/ conceal cchar=�� 538syn match IsabelleSpecial /\\<XX>/ conceal cchar=���� 539syn match IsabelleSpecial /\\<parallel>/ conceal cchar=��� 540syn match IsabelleSpecial /\\<K>/ conceal cchar=���� 541syn match IsabelleSpecial /\\<nn>/ conceal cchar=���� 542syn match IsabelleSpecial /\\<registered>/ conceal cchar=�� 543syn match IsabelleSpecial /\\<M>/ conceal cchar=��� 544syn match IsabelleSpecial /\\<delta>/ conceal cchar=�� 545syn match IsabelleSpecial /\\<threequarters>/ conceal cchar=�� 546syn match IsabelleSpecial /\\<g>/ conceal cchar=���� 547syn match IsabelleSpecial /\\<cong>/ conceal cchar=��� 548syn match IsabelleSpecial /\\<tau>/ conceal cchar=�� 549syn match IsabelleSpecial /\\<w>/ conceal cchar=���� 550syn match IsabelleSpecial /\\<ge>/ conceal cchar=��� 551syn match IsabelleSpecial /\\<flat>/ conceal cchar=��� 552syn match IsabelleSpecial /\\<zero>/ conceal cchar=���� 553syn match IsabelleSpecial /\\<Uplus>/ conceal cchar=��� 554syn match IsabelleSpecial /\\<longmapsto>/ conceal cchar=��� 555syn match IsabelleSpecial /\\<supset>/ conceal cchar=��� 556syn match IsabelleSpecial /\\<in>/ conceal cchar=��� 557syn match IsabelleSpecial /\\<sqinter>/ conceal cchar=��� 558syn match IsabelleSpecial /\\<OO>/ conceal cchar=���� 559syn match IsabelleSpecial /\\<updown>/ conceal cchar=��� 560syn match IsabelleSpecial /\\<circ>/ conceal cchar=��� 561syn match IsabelleSpecial /\\<rat>/ conceal cchar=��� 562syn match IsabelleSpecial /\\<stileturn>/ conceal cchar=��� 563syn match IsabelleSpecial /\\<ee>/ conceal cchar=���� 564syn match IsabelleSpecial /\\<Omega>/ conceal cchar=�� 565syn match IsabelleSpecial /\\<or>/ conceal cchar=��� 566syn match IsabelleSpecial /\\<inverse>/ conceal cchar=�� 567syn match IsabelleSpecial /\\<rhd>/ conceal cchar=��� 568syn match IsabelleSpecial /\\<uu>/ conceal cchar=���� 569syn match IsabelleSpecial /\\<iota>/ conceal cchar=�� 570syn match IsabelleSpecial /\\<d>/ conceal cchar=���� 571syn match IsabelleSpecial /\\<questiondown>/ conceal cchar=�� 572syn match IsabelleSpecial /\\<Union>/ conceal cchar=��� 573syn match IsabelleSpecial /\\<omega>/ conceal cchar=�� 574syn match IsabelleSpecial /\\<approx>/ conceal cchar=��� 575syn match IsabelleSpecial /\\<t>/ conceal cchar=���� 576syn match IsabelleSpecial /\\<Updown>/ conceal cchar=��� 577syn match IsabelleSpecial /\\<spadesuit>/ conceal cchar=��� 578syn match IsabelleSpecial /\\<five>/ conceal cchar=���� 579syn match IsabelleSpecial /\\<exists>/ conceal cchar=��� 580syn match IsabelleSpecial /\\<rceil>/ conceal cchar=��� 581syn match IsabelleSpecial /\\<JJ>/ conceal cchar=���� 582syn match IsabelleSpecial /\\<minusplus>/ conceal cchar=��� 583syn match IsabelleSpecial /\\<nat>/ conceal cchar=��� 584syn match IsabelleSpecial /\\<oslash>/ conceal cchar=��� 585syn match IsabelleSpecial /\\<A>/ conceal cchar=���� 586syn match IsabelleSpecial /\\<Xi>/ conceal cchar=�� 587syn match IsabelleSpecial /\\<currency>/ conceal cchar=�� 588syn match IsabelleSpecial /\\<Turnstile>/ conceal cchar=��� 589syn match IsabelleSpecial /\\<hookrightarrow>/ conceal cchar=��� 590syn match IsabelleSpecial /\\<pp>/ conceal cchar=���� 591syn match IsabelleSpecial /\\<Q>/ conceal cchar=���� 592syn match IsabelleSpecial /\\<aleph>/ conceal cchar=��� 593syn match IsabelleSpecial /\\<acute>/ conceal cchar=�� 594syn match IsabelleSpecial /\\<xi>/ conceal cchar=�� 595syn match IsabelleSpecial /\\<simeq>/ conceal cchar=��� 596syn match IsabelleSpecial /\\<i>/ conceal cchar=���� 597syn match IsabelleSpecial /\\<Join>/ conceal cchar=��� 598syn match IsabelleSpecial /\\<y>/ conceal cchar=���� 599syn match IsabelleSpecial /\\<lbrakk>/ conceal cchar=��� 600syn match IsabelleSpecial /\\<greatersim>/ conceal cchar=��� 601syn match IsabelleSpecial /\\<greaterapprox>/ conceal cchar=��� 602syn match IsabelleSpecial /\\<longrightarrow>/ conceal cchar=��� 603syn match IsabelleSpecial /\\<lceil>/ conceal cchar=��� 604syn match IsabelleSpecial /\\<Gamma>/ conceal cchar=�� 605syn match IsabelleSpecial /\\<odot>/ conceal cchar=��� 606syn match IsabelleSpecial /\\<YY>/ conceal cchar=���� 607syn match IsabelleSpecial /\\<infinity>/ conceal cchar=��� 608syn match IsabelleSpecial /\\<Sigma>/ conceal cchar=�� 609syn match IsabelleSpecial /\\<yen>/ conceal cchar=�� 610syn match IsabelleSpecial /\\<int>/ conceal cchar=��� 611syn match IsabelleSpecial /\\<tturnstile>/ conceal cchar=��� 612syn match IsabelleSpecial /\\<oo>/ conceal cchar=���� 613syn match IsabelleSpecial /\\<ointegral>/ conceal cchar=��� 614syn match IsabelleSpecial /\\<gamma>/ conceal cchar=�� 615syn match IsabelleSpecial /\\<upharpoonleft>/ conceal cchar=��� 616syn match IsabelleSpecial /\\<sigma>/ conceal cchar=�� 617syn match IsabelleSpecial /\\<n>/ conceal cchar=���� 618syn match IsabelleSpecial /\\<rbrace>/ conceal cchar=��� 619syn match IsabelleSpecial /\\<DD>/ conceal cchar=���� 620syn match IsabelleSpecial /\\<notin>/ conceal cchar=��� 621syn match IsabelleSpecial /\\<j>/ conceal cchar=���� 622syn match IsabelleSpecial /\\<uplus>/ conceal cchar=��� 623syn match IsabelleSpecial /\\<leftrightarrow>/ conceal cchar=��� 624syn match IsabelleSpecial /\\<TT>/ conceal cchar=���� 625syn match IsabelleSpecial /\\<bullet>/ conceal cchar=��� 626syn match IsabelleSpecial /\\<Theta>/ conceal cchar=�� 627syn match IsabelleSpecial /\\<smile>/ conceal cchar=��� 628syn match IsabelleSpecial /\\<G>/ conceal cchar=���� 629syn match IsabelleSpecial /\\<jj>/ conceal cchar=���� 630syn match IsabelleSpecial /\\<inter>/ conceal cchar=��� 631syn match IsabelleSpecial /\\<Psi>/ conceal cchar=�� 632syn match IsabelleSpecial /\\<ordfeminine>/ conceal cchar=�� 633syn match IsabelleSpecial /\\<W>/ conceal cchar=���� 634syn match IsabelleSpecial /\\<zz>/ conceal cchar=���� 635syn match IsabelleSpecial /\\<theta>/ conceal cchar=�� 636syn match IsabelleSpecial /\\<ordmasculine>/ conceal cchar=�� 637syn match IsabelleSpecial /\\<c>/ conceal cchar=���� 638syn match IsabelleSpecial /\\<psi>/ conceal cchar=�� 639syn match IsabelleSpecial /\\<s>/ conceal cchar=���� 640syn match IsabelleSpecial /\\<Leftrightarrow>/ conceal cchar=��� 641syn match IsabelleSpecial /\\<heartsuit>/ conceal cchar=��� 642syn match IsabelleSpecial /\\<four>/ conceal cchar=���� 643syn match IsabelleSpecial /\\<open>/ conceal cchar=��� transparent 644syn match IsabelleSpecial /\\<close>/ conceal cchar=��� transparent 645syn match IsabelleSpecial /\\<comment>/ conceal cchar=��� transparent 646 647syn cluster IsabelleInnerStuff contains=IsabelleSpecial,IsabelleComment 648 649" Enable folding of proofs and locales. Note that the starting regex needs to 650" match with zero width to preserve syntax highlighting of the opening command. 651syn region IsabelleLemmaFold 652 \ start="\(\<\(schematic_\)\?\(corollary\|lemma\|theorem\)\>\|have\|show\)\@<=" 653 \ end="\<\(done\|by\|qed\|apply_end\|oops\|sorry\)\>" 654 \ fold keepend transparent 655syn region IsabelleLocaleFold 656 \ start="\(\<\(sub\)\?locale\>\)\@<=" 657 \ end="\<end\>" 658 \ fold keepend transparent 659 660syn match IsabelleComment "--.*$" 661hi def link IsabelleComment Comment 662hi def link IsabelleCommentStart Comment 663hi def link IsabelleCommentContent Comment 664 665hi IsabelleCommand ctermfg=3 cterm=bold guifg=yellow gui=bold 666hi IsabelleCommandPart ctermfg=3 cterm=none guifg=yellow 667hi IsabelleCommandMod ctermfg=3 cterm=none guifg=yellow 668hi IsabelleInnerMarker ctermfg=1 cterm=none guifg=red 669hi IsabelleSpecial ctermfg=5 cterm=none guifg=magenta 670hi IsabelleCommandProofProve ctermfg=2 cterm=none guifg=green 671hi IsabelleCommandProofIsar ctermfg=2 cterm=none guifg=green 672hi IsabelleGoalProofIsar ctermfg=3 cterm=none guifg=yellow 673hi IsabelleCommandProofDone ctermfg=2 cterm=bold guifg=green gui=bold 674hi IsabelleCommandProofFail ctermfg=1 cterm=bold guifg=red gui=bold 675hi IsabelleCommandProofBad ctermfg=1 cterm=none guifg=red 676hi IsabelleCommandRule ctermfg=7 cterm=bold guifg=white gui=bold 677hi IsabelleCommandRuleMod ctermfg=6 cterm=none guifg=cyan 678hi IsabelleCommandMethod ctermfg=6 cterm=none guifg=cyan 679hi IsabelleCommandMethodMod ctermfg=6 cterm=none guifg=cyan 680hi IsabelleCommandBigMethod ctermfg=6 cterm=bold guifg=cyan gui=bold 681 682hi Normal guibg=black guifg=grey 683 684" Jedit-style autocompletion. This is off by default because it can 685" significantly slow Vim down. To use this functionality, put something like 686" the following in your ~/.vimrc and then use F9 to toggle completion on and 687" off. 688" 689" function! ToggleIsabelleAbbreviations() 690" if exists('g:isabelle_abbreviations') 691" let g:isabelle_abbreviations=!g:isabelle_abbreviations 692" else 693" let g:isabelle_abbreviations=1 694" endif 695" syntax off 696" syntax on 697" endfunction 698" nm <F9> :call ToggleIsabelleAbbreviations()<CR> 699" imap <F9> <C-o>:call ToggleIsabelleAbbreviations()<CR> 700" 701if exists('g:isabelle_abbreviations') 702 if g:isabelle_abbreviations == 1 703 " Tweak the things that Vim sees as part of a word. This is useful if you 704 " have macros that kick in on word completion or similar. 705 set iskeyword+=> 706 set iskeyword+=] 707 set iskeyword+=: 708 " XXX: Vim does not seem to have a way to add '*' to the iskeyword set. 709 710 " Jedit-style autocomplete of unicode tokens. This was generated by the 711 " following Python 712 " 713 " import isasymbols # From l4v-internal 714 " 715 " def vim_escape(data): 716 " 'Escape characters that are special to Vim' 717 " return data.replace('<', '<lt>').replace('\\', 718 " '<Bslash>').replace('|', '<Bar>') 719 " 720 " t = isasymbols.make_translator('/path/to/symbols') 721 " for symbol in t.symbols: 722 " for abbreviation in symbol.abbreviations: 723 " print 'iab %s %s' % (vim_escape(abbreviation), 724 " vim_escape(symbol.ascii_text)) 725 " 726 iab <buffer> % <Bslash><lt>lambda> 727 iab <buffer> <lt>. <Bslash><lt>leftarrow> 728 iab <buffer> <lt>. <Bslash><lt>longleftarrow> 729 iab <buffer> .> <Bslash><lt>rightarrow> 730 iab <buffer> -> <Bslash><lt>rightarrow> 731 iab <buffer> .> <Bslash><lt>longrightarrow> 732 iab <buffer> --> <Bslash><lt>longrightarrow> 733 iab <buffer> <lt>. <Bslash><lt>Leftarrow> 734 iab <buffer> <lt>. <Bslash><lt>Longleftarrow> 735 iab <buffer> .> <Bslash><lt>Rightarrow> 736 iab <buffer> => <Bslash><lt>Rightarrow> 737 iab <buffer> .> <Bslash><lt>Longrightarrow> 738 iab <buffer> ==> <Bslash><lt>Longrightarrow> 739 iab <buffer> <lt>> <Bslash><lt>leftrightarrow> 740 iab <buffer> <lt>-> <Bslash><lt>leftrightarrow> 741 iab <buffer> <lt>> <Bslash><lt>longleftrightarrow> 742 iab <buffer> <lt>-> <Bslash><lt>longleftrightarrow> 743 iab <buffer> <lt>--> <Bslash><lt>longleftrightarrow> 744 iab <buffer> <lt>> <Bslash><lt>Leftrightarrow> 745 iab <buffer> <lt>> <Bslash><lt>Longleftrightarrow> 746 iab <buffer> .> <Bslash><lt>mapsto> 747 iab <buffer> <Bar>-> <Bslash><lt>mapsto> 748 iab <buffer> .> <Bslash><lt>longmapsto> 749 iab <buffer> <Bar>--> <Bslash><lt>longmapsto> 750 iab <buffer> <lt>> <Bslash><lt>midarrow> 751 iab <buffer> <lt>> <Bslash><lt>Midarrow> 752 iab <buffer> <lt>. <Bslash><lt>hookleftarrow> 753 iab <buffer> .> <Bslash><lt>hookrightarrow> 754 iab <buffer> <lt>. <Bslash><lt>leftharpoondown> 755 iab <buffer> .> <Bslash><lt>rightharpoondown> 756 iab <buffer> <lt>. <Bslash><lt>leftharpoonup> 757 iab <buffer> .> <Bslash><lt>rightharpoonup> 758 iab <buffer> <lt>> <Bslash><lt>rightleftharpoons> 759 iab <buffer> == <Bslash><lt>rightleftharpoons> 760 iab <buffer> .> <Bslash><lt>leadsto> 761 iab <buffer> ~> <Bslash><lt>leadsto> 762 iab <buffer> <lt><lt> <Bslash><lt>langle> 763 iab <buffer> >> <Bslash><lt>rangle> 764 iab <buffer> [. <Bslash><lt>lceil> 765 iab <buffer> .] <Bslash><lt>rceil> 766 iab <buffer> [. <Bslash><lt>lfloor> 767 iab <buffer> .] <Bslash><lt>rfloor> 768 iab <buffer> (<Bar> <Bslash><lt>lparr> 769 iab <buffer> <Bar>) <Bslash><lt>rparr> 770 iab <buffer> [<Bar> <Bslash><lt>lbrakk> 771 iab <buffer> <Bar>] <Bslash><lt>rbrakk> 772 iab <buffer> {<Bar> <Bslash><lt>lbrace> 773 iab <buffer> <Bar>} <Bslash><lt>rbrace> 774 iab <buffer> <lt><lt> <Bslash><lt>guillemotleft> 775 iab <buffer> >> <Bslash><lt>guillemotright> 776 iab <buffer> /<Bslash> <Bslash><lt>and> 777 iab <buffer> & <Bslash><lt>and> 778 iab <buffer> !! <Bslash><lt>And> 779 iab <buffer> <Bslash>/ <Bslash><lt>or> 780 iab <buffer> <Bar> <Bslash><lt>or> 781 iab <buffer> ?? <Bslash><lt>Or> 782 iab <buffer> ! <Bslash><lt>forall> 783 iab <buffer> ALL <Bslash><lt>forall> 784 iab <buffer> ? <Bslash><lt>exists> 785 iab <buffer> EX <Bslash><lt>exists> 786 iab <buffer> ~? <Bslash><lt>nexists> 787 iab <buffer> ~ <Bslash><lt>not> 788 iab <buffer> <Bar>- <Bslash><lt>turnstile> 789 iab <buffer> <Bar>= <Bslash><lt>Turnstile> 790 iab <buffer> <Bar>- <Bslash><lt>tturnstile> 791 iab <buffer> <Bar>= <Bslash><lt>TTurnstile> 792 iab <buffer> -<Bar> <Bslash><lt>stileturn> 793 iab <buffer> <lt>= <Bslash><lt>le> 794 iab <buffer> >= <Bslash><lt>ge> 795 iab <buffer> <lt><lt> <Bslash><lt>lless> 796 iab <buffer> >> <Bslash><lt>ggreater> 797 iab <buffer> : <Bslash><lt>in> 798 iab <buffer> ~: <Bslash><lt>notin> 799 iab <buffer> (= <Bslash><lt>subseteq> 800 iab <buffer> )= <Bslash><lt>supseteq> 801 iab <buffer> [= <Bslash><lt>sqsubseteq> 802 iab <buffer> ]= <Bslash><lt>sqsupseteq> 803 iab <buffer> Int <Bslash><lt>inter> 804 iab <buffer> Inter <Bslash><lt>Inter> 805 iab <buffer> INT <Bslash><lt>Inter> 806 iab <buffer> Un <Bslash><lt>union> 807 iab <buffer> Union <Bslash><lt>Union> 808 iab <buffer> UN <Bslash><lt>Union> 809 iab <buffer> SUP <Bslash><lt>Squnion> 810 iab <buffer> INF <Bslash><lt>Sqinter> 811 iab <buffer> ~= <Bslash><lt>noteq> 812 iab <buffer> .= <Bslash><lt>doteq> 813 iab <buffer> == <Bslash><lt>equiv> 814 iab <buffer> <Bar><Bar> <Bslash><lt>parallel> 815 iab <buffer> <Bar><Bar> <Bslash><lt>bar> 816 iab <buffer> <lt>*> <Bslash><lt>times> 817 iab <buffer> +o <Bslash><lt>oplus> 818 iab <buffer> +O <Bslash><lt>Oplus> 819 iab <buffer> *o <Bslash><lt>otimes> 820 iab <buffer> *O <Bslash><lt>Otimes> 821 iab <buffer> .o <Bslash><lt>odot> 822 iab <buffer> .O <Bslash><lt>Odot> 823 iab <buffer> -o <Bslash><lt>ominus> 824 iab <buffer> /o <Bslash><lt>oslash> 825 iab <buffer> ... <Bslash><lt>dots> 826 iab <buffer> SUM <Bslash><lt>Sum> 827 iab <buffer> PROD <Bslash><lt>Prod> 828 iab <buffer> <lt><lt> <Bslash><lt>open> 829 iab <buffer> >> <Bslash><lt>close> 830 iab <buffer> =_( <Bslash><lt>^bsub> 831 iab <buffer> =_) <Bslash><lt>^esub> 832 iab <buffer> =^( <Bslash><lt>^bsup> 833 iab <buffer> =^) <Bslash><lt>^esup> 834 else 835 " Reset to default. 836 set iskeyword=@,48-57,_,192-255 837 838 " Remove all abbreviations. 839 iabc <buffer> 840 endif 841endif 842