# HG changeset patch # User wenzelm # Date 1191756737 -7200 # Node ID 173f23cecbe8f1da2cea83408900772062acd7c1 # Parent ce449d6aef3fb95323f85485a730be18b0795626 isabelle mode for jEdit; diff -r ce449d6aef3f -r 173f23cecbe8 lib/jedit/isabelle.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/jedit/isabelle.xml Sun Oct 07 13:32:17 2007 +0200 @@ -0,0 +1,335 @@ + + + + + + + + + + + + + + + + + (* + *) + + + {* + *} + + + ` + ` + + + " + " + + + . + .. + + + ML_setup + abbreviation + actions + advanced + also + and + apply + apply_end + arities + assume + assumes + atom_decl + attach + automaton + avoids + ax_specification + axclass + axiomatization + axioms + back + begin + binder + by + cannot_undo + case + case_eqns + + chapter + class + + classes + classrel + codatatype + code_class + code_const + code_datatype + + code_exception + code_instance + code_library + code_module + code_modulename + code_moduleprolog + code_monad + code_props + code_reserved + + code_type + coinductive + coinductive_set + + compose + con_defs + concl + congs + constdefs + constrains + consts + consts_code + contains + context + corollary + cpodef + datatype + declaration + declare + def + defaultsort + defer + defer_recdef + defines + definition + defs + + + distinct + domain + domains + done + elimination + + end + equivariance + exit + + extract + extract_type + file + finalconsts + finally + + fix + fixes + fixpat + fixrec + for + freshness_context + from + + fun + function + global + guess + have + + + hence + hide + hide_action + hints + identifier + if + imports + in + includes + induction + inductive + inductive_cases + inductive_set + infix + infixl + infixr + init_toplevel + initially + inject + inputs + instance + instance_proof + instantiation + internals + interpret + interpretation + intros + invariant + invoke + is + judgment + kill + + lazy + lemma + lemmas + let + local + local_syntax + locale + method_setup + module_name + monos + moreover + morphisms + next + no_syntax + no_translations + nominal_datatype + nominal_inductive + nominal_primrec + nonterminals + + notation + note + notes + obtain + obtains + oops + open + oracle + otherwise + output + outputs + overloaded + parse_ast_translation + parse_translation + pcpodef + permissive + post + + pre + prefer + presume + + + primrec + + + print_ast_translation + + + + + + + + + + + + + + + + + + + + + + + + + + + + print_translation + proof + + + qed + + quickcheck_params + quit + realizability + realizers + recdef + recdef_tc + record + recursor_eqns + redo + + refute_params + + rename + rep_datatype + restrict + sect + section + sequential + setup + show + shows + signature + simproc_setup + + sorry + specification + states + structure + subsect + subsection + subsubsect + subsubsection + syntax + + termination + text + text_raw + then + theorem + theorems + theory + + + thus + + to + token_translation + + + transitions + translations + transrel + txt + txt_raw + + type_elims + type_intros + typed_print_translation + typedecl + typedef + types + types_code + ultimately + unchecked + undo + undos_proof + unfolding + + + uses + using + + + where + with + { + } + + +