isabelle: etc/isar-keywords.el@e2511e6e5cbb (annotated)

11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	1	;;
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	2	;; Keyword classification tables for Isabelle/Isar.
17552 744924bec974 Added new "value" command. berghofe parents: 17473 diff changeset	3	;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	4	;;
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	5	;; $Id$
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	6	;;
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	7
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	8	(defconst isar-keywords-major
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	9	'("\\."
15762 13d1ec61bc89 updated; wenzelm parents: 15703 diff changeset	10	"\\.\\."
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	11	"ML"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	12	"ML_command"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	13	"ML_setup"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	14	"ProofGeneral\\.inform_file_processed"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	15	"ProofGeneral\\.inform_file_retracted"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	16	"ProofGeneral\\.kill_proof"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	17	"ProofGeneral\\.process_pgip"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	18	"ProofGeneral\\.restart"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	19	"ProofGeneral\\.undo"
19069 a4b956f8b233 updated; wenzelm parents: 18888 diff changeset	20	"abbreviation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	21	"also"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	22	"apply"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	23	"apply_end"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	24	"arities"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	25	"assume"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	26	"automaton"
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	27	"ax_specification"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	28	"axclass"
18612 7300f75028dc updated; wenzelm parents: 18552 diff changeset	29	"axiomatization"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	30	"axioms"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	31	"back"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	32	"by"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	33	"cannot_undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	34	"case"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	35	"cd"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	36	"chapter"
18552 30911da9fb27 class now a keyword haftmann parents: 18541 diff changeset	37	"class"
20568 9b7f59c1bdfc updated; wenzelm parents: 20523 diff changeset	38	"class_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	39	"classes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	40	"classrel"
20931 19d9b78218fd added code_abstype and code_constsubst haftmann parents: 20832 diff changeset	41	"code_abstype"
21057 c45591716692 code_constsubst -> code_axioms haftmann parents: 21028 diff changeset	42	"code_axioms"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	43	"code_class"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	44	"code_const"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	45	"code_datatype"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	46	"code_deps"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	47	"code_gen"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	48	"code_instance"
17147 fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	49	"code_library"
fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	50	"code_module"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	51	"code_modulename"
8154a62bb498 updated; wenzelm parents: 21057 diff changeset	52	"code_moduleprolog"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	53	"code_monad"
21028 ed94ba513989 updated; wenzelm parents: 21027 diff changeset	54	"code_reserved"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	55	"code_thms"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	56	"code_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	57	"coinductive"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	58	"coinductive2"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	59	"commit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	60	"constdefs"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	61	"consts"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	62	"consts_code"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	63	"context"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	64	"corollary"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	65	"cpodef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	66	"datatype"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	67	"declaration"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	68	"declare"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	69	"def"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	70	"defaultsort"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	71	"defer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	72	"defer_recdef"
18775 becdbf57eeb8 updated; wenzelm parents: 18757 diff changeset	73	"definition"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	74	"defs"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	75	"disable_pr"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	76	"display_drafts"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	77	"domain"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	78	"done"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	79	"enable_pr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	80	"end"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	81	"exit"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	82	"extract"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	83	"extract_type"
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	84	"finalconsts"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	85	"finally"
17220 b41d8e290bf8 updated; wenzelm parents: 17147 diff changeset	86	"find_theorems"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	87	"fix"
16419 0c3db621bbbd updated; wenzelm parents: 16231 diff changeset	88	"fixpat"
16231 91c0a3e253b1 add keywords fixrec and fixpat for HOLCF fixrec package huffman parents: 16168 diff changeset	89	"fixrec"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	90	"from"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	91	"full_prf"
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: 20453 diff changeset	92	"fun"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	93	"function"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	94	"global"
17850 6803625e71c4 updated; wenzelm parents: 17552 diff changeset	95	"guess"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	96	"have"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	97	"header"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	98	"help"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	99	"hence"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	100	"hide"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	101	"inductive"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	102	"inductive2"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	103	"inductive_cases"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	104	"inductive_cases2"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	105	"init_toplevel"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	106	"instance"
15624 484178635bd8 Further work on interpretation commands. New command `interpret' for ballarin parents: 15598 diff changeset	107	"interpret"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	108	"interpretation"
19797 a527b3e1076a updated; wenzelm parents: 19655 diff changeset	109	"invoke"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	110	"judgment"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	111	"kill"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	112	"kill_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	113	"lemma"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	114	"lemmas"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	115	"let"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	116	"local"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	117	"locale"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	118	"method_setup"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	119	"moreover"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	120	"next"
15703 727ef1b8b3ee * empty log message * wenzelm parents: 15624 diff changeset	121	"no_syntax"
19255 e80e3fdda606 updated; wenzelm parents: 19149 diff changeset	122	"no_translations"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	123	"nonterminals"
19854 9c1732a66b0b updated keywords haftmann parents: 19797 diff changeset	124	"normal_form"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	125	"notation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	126	"note"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	127	"obtain"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	128	"oops"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	129	"oracle"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	130	"parse_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	131	"parse_translation"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	132	"pcpodef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	133	"pr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	134	"prefer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	135	"presume"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	136	"pretty_setmargin"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	137	"prf"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	138	"primrec"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	139	"print_abbrevs"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	140	"print_antiquotations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	141	"print_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	142	"print_attributes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	143	"print_binds"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	144	"print_cases"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	145	"print_claset"
20378 63a0aafc89ba updated code generator keywords haftmann parents: 20358 diff changeset	146	"print_classes"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	147	"print_codesetup"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	148	"print_commands"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	149	"print_context"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	150	"print_drafts"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	151	"print_facts"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	152	"print_induct_rules"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	153	"print_interps"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	154	"print_locale"
c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	155	"print_locales"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	156	"print_methods"
12365 a90156701dad updated; wenzelm parents: 12342 diff changeset	157	"print_rules"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	158	"print_simpset"
19272 5f376320109a updated; wenzelm parents: 19255 diff changeset	159	"print_statement"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	160	"print_syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	161	"print_theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	162	"print_theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	163	"print_trans_rules"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	164	"print_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	165	"proof"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	166	"prop"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	167	"pwd"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	168	"qed"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	169	"quickcheck"
7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	170	"quickcheck_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	171	"quit"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	172	"realizability"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	173	"realizers"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	174	"recdef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	175	"recdef_tc"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	176	"record"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	177	"redo"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	178	"refute"
8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	179	"refute_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	180	"remove_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	181	"rep_datatype"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	182	"sect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	183	"section"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	184	"setup"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	185	"show"
22200 d4797b506752 updated; wenzelm parents: 22084 diff changeset	186	"simproc_setup"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	187	"sledgehammer"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	188	"sorry"
14115 65ec3f73d00b Added package for definition by specification. skalberg parents: 14109 diff changeset	189	"specification"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	190	"subsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	191	"subsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	192	"subsubsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	193	"subsubsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	194	"syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	195	"term"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	196	"termination"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	197	"text"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	198	"text_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	199	"then"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	200	"theorem"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	201	"theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	202	"theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	203	"thm"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	204	"thm_deps"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	205	"thus"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	206	"thy_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	207	"token_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	208	"touch_all_thys"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	209	"touch_child_thys"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	210	"touch_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	211	"translations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	212	"txt"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	213	"txt_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	214	"typ"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	215	"typed_print_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	216	"typedecl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	217	"typedef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	218	"types"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	219	"types_code"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	220	"ultimately"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	221	"undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	222	"undos_proof"
18541 00890455e95f updated -- lost update!? wenzelm parents: 18520 diff changeset	223	"unfolding"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	224	"update_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	225	"update_thy_only"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	226	"use"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	227	"use_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	228	"use_thy_only"
12926 cd0dd6e0bf5c 'using' command; wenzelm parents: 12365 diff changeset	229	"using"
17552 744924bec974 Added new "value" command. berghofe parents: 17473 diff changeset	230	"value"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	231	"welcome"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	232	"with"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	233	"{"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	234	"}"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	235
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	236	(defconst isar-keywords-minor
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	237	'("actions"
14660 934e03881ad6 updated -- too late for Isabelle2004! wenzelm parents: 14508 diff changeset	238	"advanced"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	239	"and"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	240	"assumes"
16771 2b534c5b5625 Added "attach" keyword for code generator setup. berghofe parents: 16701 diff changeset	241	"attach"
15135 f00857c7539b Added "import" and "begin" nipkow parents: 14938 diff changeset	242	"begin"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	243	"binder"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	244	"compose"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	245	"concl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	246	"congs"
16168 adb83939177f Locales: new element constrains, parameter renaming with syntax, ballarin parents: 16034 diff changeset	247	"constrains"
17147 fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	248	"contains"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	249	"defines"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	250	"distinct"
17147 fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	251	"file"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	252	"fixes"
19797 a527b3e1076a updated; wenzelm parents: 19655 diff changeset	253	"for"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	254	"hide_action"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	255	"hints"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	256	"identifier"
19797 a527b3e1076a updated; wenzelm parents: 19655 diff changeset	257	"if"
15141 a95c2ff210ba import -> imports nipkow parents: 15135 diff changeset	258	"imports"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	259	"in"
12954 850609c057e2 updated; wenzelm parents: 12935 diff changeset	260	"includes"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	261	"induction"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	262	"infix"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	263	"infixl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	264	"infixr"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	265	"initially"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	266	"inject"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	267	"inputs"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	268	"internals"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	269	"intros"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	270	"is"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	271	"lazy"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	272	"monos"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	273	"morphisms"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	274	"notes"
18888 3b643f81b378 updated; wenzelm parents: 18775 diff changeset	275	"obtains"
13364 d3c7d05d8839 updated; wenzelm parents: 12954 diff changeset	276	"open"
20338 ecdfc96cf4d0 Added Keywords: "otherwise" and "sequential", needed for function package's krauss parents: 19891 diff changeset	277	"otherwise"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	278	"output"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	279	"outputs"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	280	"overloaded"
11618 7067101463c0 updated; wenzelm parents: 11538 diff changeset	281	"permissive"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	282	"post"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	283	"pre"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	284	"rename"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	285	"restrict"
20338 ecdfc96cf4d0 Added Keywords: "otherwise" and "sequential", needed for function package's krauss parents: 19891 diff changeset	286	"sequential"
12935 d697091d1591 updated; wenzelm parents: 12926 diff changeset	287	"shows"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	288	"signature"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	289	"states"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	290	"structure"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	291	"to"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	292	"transitions"
61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	293	"transrel"
19633 a6fad1e8bbd2 updated; wenzelm parents: 19564 diff changeset	294	"unchecked"
16419 0c3db621bbbd updated; wenzelm parents: 16231 diff changeset	295	"uses"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	296	"where"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	297
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	298	(defconst isar-keywords-control
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	299	'("ProofGeneral\\.inform_file_processed"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	300	"ProofGeneral\\.inform_file_retracted"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	301	"ProofGeneral\\.kill_proof"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	302	"ProofGeneral\\.process_pgip"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	303	"ProofGeneral\\.restart"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	304	"ProofGeneral\\.undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	305	"cannot_undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	306	"exit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	307	"init_toplevel"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	308	"kill"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	309	"quit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	310	"redo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	311	"undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	312	"undos_proof"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	313
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	314	(defconst isar-keywords-diag
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	315	'("ML"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	316	"ML_command"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	317	"cd"
20568 9b7f59c1bdfc updated; wenzelm parents: 20523 diff changeset	318	"class_deps"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	319	"code_deps"
20586 548fd4cd2eb3 code_gen now peek keyword haftmann parents: 20568 diff changeset	320	"code_gen"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	321	"code_thms"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	322	"commit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	323	"disable_pr"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	324	"display_drafts"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	325	"enable_pr"
17220 b41d8e290bf8 updated; wenzelm parents: 17147 diff changeset	326	"find_theorems"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	327	"full_prf"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	328	"header"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	329	"help"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	330	"kill_thy"
20832 c3828205f22d normal_form now a diagnostic command haftmann parents: 20697 diff changeset	331	"normal_form"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	332	"pr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	333	"pretty_setmargin"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	334	"prf"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	335	"print_abbrevs"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	336	"print_antiquotations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	337	"print_attributes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	338	"print_binds"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	339	"print_cases"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	340	"print_claset"
20378 63a0aafc89ba updated code generator keywords haftmann parents: 20358 diff changeset	341	"print_classes"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	342	"print_codesetup"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	343	"print_commands"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	344	"print_context"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	345	"print_drafts"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	346	"print_facts"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	347	"print_induct_rules"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	348	"print_interps"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	349	"print_locale"
c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	350	"print_locales"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	351	"print_methods"
12365 a90156701dad updated; wenzelm parents: 12342 diff changeset	352	"print_rules"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	353	"print_simpset"
19272 5f376320109a updated; wenzelm parents: 19255 diff changeset	354	"print_statement"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	355	"print_syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	356	"print_theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	357	"print_theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	358	"print_trans_rules"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	359	"prop"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	360	"pwd"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	361	"quickcheck"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	362	"refute"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	363	"remove_thy"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	364	"sledgehammer"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	365	"term"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	366	"thm"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	367	"thm_deps"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	368	"thy_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	369	"touch_all_thys"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	370	"touch_child_thys"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	371	"touch_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	372	"typ"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	373	"update_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	374	"update_thy_only"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	375	"use"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	376	"use_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	377	"use_thy_only"
17552 744924bec974 Added new "value" command. berghofe parents: 17473 diff changeset	378	"value"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	379	"welcome"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	380
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	381	(defconst isar-keywords-theory-begin
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	382	'("theory"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	383
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	384	(defconst isar-keywords-theory-switch
21302 4c8f3dfc7124 updated; wenzelm parents: 21203 diff changeset	385	'())
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	386
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	387	(defconst isar-keywords-theory-end
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	388	'("end"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	389
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	390	(defconst isar-keywords-theory-heading
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	391	'("chapter"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	392	"section"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	393	"subsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	394	"subsubsection"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	395
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	396	(defconst isar-keywords-theory-decl
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	397	'("ML_setup"
19069 a4b956f8b233 updated; wenzelm parents: 18888 diff changeset	398	"abbreviation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	399	"arities"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	400	"automaton"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	401	"axclass"
18612 7300f75028dc updated; wenzelm parents: 18552 diff changeset	402	"axiomatization"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	403	"axioms"
18552 30911da9fb27 class now a keyword haftmann parents: 18541 diff changeset	404	"class"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	405	"classes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	406	"classrel"
20931 19d9b78218fd added code_abstype and code_constsubst haftmann parents: 20832 diff changeset	407	"code_abstype"
21057 c45591716692 code_constsubst -> code_axioms haftmann parents: 21028 diff changeset	408	"code_axioms"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	409	"code_class"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	410	"code_const"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	411	"code_datatype"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	412	"code_instance"
17147 fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	413	"code_library"
fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	414	"code_module"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	415	"code_modulename"
8154a62bb498 updated; wenzelm parents: 21057 diff changeset	416	"code_moduleprolog"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	417	"code_monad"
21028 ed94ba513989 updated; wenzelm parents: 21027 diff changeset	418	"code_reserved"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	419	"code_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	420	"coinductive"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	421	"coinductive2"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	422	"constdefs"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	423	"consts"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	424	"consts_code"
21302 4c8f3dfc7124 updated; wenzelm parents: 21203 diff changeset	425	"context"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	426	"datatype"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	427	"declaration"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	428	"defaultsort"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	429	"defer_recdef"
18775 becdbf57eeb8 updated; wenzelm parents: 18757 diff changeset	430	"definition"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	431	"defs"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	432	"domain"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	433	"extract"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	434	"extract_type"
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	435	"finalconsts"
16419 0c3db621bbbd updated; wenzelm parents: 16231 diff changeset	436	"fixpat"
16231 91c0a3e253b1 add keywords fixrec and fixpat for HOLCF fixrec package huffman parents: 16168 diff changeset	437	"fixrec"
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: 20453 diff changeset	438	"fun"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	439	"global"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	440	"hide"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	441	"inductive"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	442	"inductive2"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	443	"judgment"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	444	"lemmas"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	445	"local"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	446	"locale"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	447	"method_setup"
15703 727ef1b8b3ee * empty log message * wenzelm parents: 15624 diff changeset	448	"no_syntax"
19255 e80e3fdda606 updated; wenzelm parents: 19149 diff changeset	449	"no_translations"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	450	"nonterminals"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	451	"notation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	452	"oracle"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	453	"parse_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	454	"parse_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	455	"primrec"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	456	"print_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	457	"print_translation"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	458	"quickcheck_params"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	459	"realizability"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	460	"realizers"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	461	"recdef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	462	"record"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	463	"refute_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	464	"rep_datatype"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	465	"setup"
22200 d4797b506752 updated; wenzelm parents: 22084 diff changeset	466	"simproc_setup"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	467	"syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	468	"text"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	469	"text_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	470	"theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	471	"token_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	472	"translations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	473	"typed_print_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	474	"typedecl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	475	"types"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	476	"types_code"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	477
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	478	(defconst isar-keywords-theory-script
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	479	'("declare"
21027 3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	480	"inductive_cases"
3f89f99d746e Added keywords for new inductive definition package. berghofe parents: 20931 diff changeset	481	"inductive_cases2"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	482
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	483	(defconst isar-keywords-theory-goal
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	484	'("ax_specification"
0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	485	"corollary"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	486	"cpodef"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	487	"function"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	488	"instance"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	489	"interpretation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	490	"lemma"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	491	"pcpodef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	492	"recdef_tc"
14115 65ec3f73d00b Added package for definition by specification. skalberg parents: 14109 diff changeset	493	"specification"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	494	"termination"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	495	"theorem"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	496	"typedef"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	497
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	498	(defconst isar-keywords-qed
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	499	'("\\."
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	500	"\\.\\."
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	501	"by"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	502	"done"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	503	"sorry"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	504
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	505	(defconst isar-keywords-qed-block
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	506	'("qed"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	507
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	508	(defconst isar-keywords-qed-global
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	509	'("oops"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	510
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	511	(defconst isar-keywords-proof-heading
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	512	'("sect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	513	"subsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	514	"subsubsect"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	515
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	516	(defconst isar-keywords-proof-goal
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	517	'("have"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	518	"hence"
15624 484178635bd8 Further work on interpretation commands. New command `interpret' for ballarin parents: 15598 diff changeset	519	"interpret"
21806 6086783d4214 updated; wenzelm parents: 21732 diff changeset	520	"invoke"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	521
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	522	(defconst isar-keywords-proof-block
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	523	'("next"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	524	"proof"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	525
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	526	(defconst isar-keywords-proof-open
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	527	'("{"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	528
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	529	(defconst isar-keywords-proof-close
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	530	'("}"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	531
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	532	(defconst isar-keywords-proof-chain
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	533	'("finally"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	534	"from"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	535	"then"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	536	"ultimately"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	537	"with"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	538
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	539	(defconst isar-keywords-proof-decl
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	540	'("also"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	541	"let"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	542	"moreover"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	543	"note"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	544	"txt"
12926 cd0dd6e0bf5c 'using' command; wenzelm parents: 12365 diff changeset	545	"txt_raw"
18541 00890455e95f updated -- lost update!? wenzelm parents: 18520 diff changeset	546	"unfolding"
12926 cd0dd6e0bf5c 'using' command; wenzelm parents: 12365 diff changeset	547	"using"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	548
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	549	(defconst isar-keywords-proof-asm
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	550	'("assume"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	551	"case"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	552	"def"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	553	"fix"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	554	"presume"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	555
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	556	(defconst isar-keywords-proof-asm-goal
17850 6803625e71c4 updated; wenzelm parents: 17552 diff changeset	557	'("guess"
21806 6086783d4214 updated; wenzelm parents: 21732 diff changeset	558	"obtain"
6086783d4214 updated; wenzelm parents: 21732 diff changeset	559	"show"
6086783d4214 updated; wenzelm parents: 21732 diff changeset	560	"thus"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	561
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	562	(defconst isar-keywords-proof-script
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	563	'("apply"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	564	"apply_end"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	565	"back"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	566	"defer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	567	"prefer"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	568
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	569	(provide 'isar-keywords)

author	wenzelm
	Tue, 08 May 2007 15:01:29 +0200
changeset 22864	e2511e6e5cbb
parent 22486	d3b6cb2306b6
child 23732	f9f89b7cfdc7
permissions	-rw-r--r--