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

11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	1	;;
52442 d3c5195b7399 misc tuning and clarification; wenzelm parents: 52439 diff changeset	2	;; Keyword classification tables for Isabelle/Isar.
53432 36ca6764027f updated keywords; wenzelm parents: 53312 diff changeset	3	;; Generated from HOL + HOL-Auth + HOL-BNF + HOL-BNF-LFP + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-ex + HOLCF + Pure.
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	5	;;
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	(defconst isar-keywords-major
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	8	'("\\."
15762 13d1ec61bc89 updated; wenzelm parents: 15703 diff changeset	9	"\\.\\."
25577 d739f48ef40c updated; wenzelm parents: 25516 diff changeset	10	"Isabelle\\.command"
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"
48867 e9beabf045ab some support for inlining file content into outer syntax token language; wenzelm parents: 48709 diff changeset	13	"ML_file"
28280 fd0485db7d5a updated generated file; wenzelm parents: 27621 diff changeset	14	"ML_prf"
26394 ddd7825ea4cd * empty log message * wenzelm parents: 26184 diff changeset	15	"ML_val"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	16	"ProofGeneral\\.inform_file_processed"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	17	"ProofGeneral\\.inform_file_retracted"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	18	"ProofGeneral\\.kill_proof"
33874 1db5ca5eadf5 updated keywords; wenzelm parents: 33840 diff changeset	19	"ProofGeneral\\.pr"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	20	"ProofGeneral\\.process_pgip"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	21	"ProofGeneral\\.restart"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	22	"ProofGeneral\\.undo"
19069 a4b956f8b233 updated; wenzelm parents: 18888 diff changeset	23	"abbreviation"
52623 fee0db8cf60d updated keywords; wenzelm parents: 52549 diff changeset	24	"adhoc_overloading"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	25	"also"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	26	"apply"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	27	"apply_end"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	28	"arities"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	29	"assume"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	30	"atom_decl"
30527 fae488569faf updated generated files; wenzelm parents: 30463 diff changeset	31	"attribute_setup"
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	32	"ax_specification"
18612 7300f75028dc updated; wenzelm parents: 18552 diff changeset	33	"axiomatization"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	34	"back"
51836 4d6dcd51dd52 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration) blanchet parents: 51804 diff changeset	35	"bnf"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	36	"bundle"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	37	"by"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	38	"cannot_undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	39	"case"
53432 36ca6764027f updated keywords; wenzelm parents: 53312 diff changeset	40	"case_of_simps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	41	"cd"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	42	"chapter"
18552 30911da9fb27 class now a keyword haftmann parents: 18541 diff changeset	43	"class"
20568 9b7f59c1bdfc updated; wenzelm parents: 20523 diff changeset	44	"class_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	45	"classes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	46	"classrel"
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51789 diff changeset	47	"codatatype"
27102 a98cd7450204 updated haftmann parents: 26896 diff changeset	48	"code_abort"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	49	"code_class"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	50	"code_const"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	51	"code_datatype"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	52	"code_deps"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	53	"code_identifier"
24997 730d74336b4d updated haftmann parents: 24945 diff changeset	54	"code_include"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	55	"code_instance"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	56	"code_modulename"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	57	"code_monad"
31106 9a1178204dc0 Added pred_code command bulwahn parents: 30856 diff changeset	58	"code_pred"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	59	"code_printing"
36472 3e677ca1e564 updated keywords haftmann parents: 36455 diff changeset	60	"code_reflect"
21028 ed94ba513989 updated; wenzelm parents: 21027 diff changeset	61	"code_reserved"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	62	"code_thms"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	63	"code_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	64	"coinductive"
23732 f9f89b7cfdc7 Adapted to changes in inductive definition package. berghofe parents: 22864 diff changeset	65	"coinductive_set"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	66	"commit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	67	"consts"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	68	"context"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	69	"corollary"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	70	"cpodef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	71	"datatype"
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51789 diff changeset	72	"datatype_new"
53312 a1cf42366cea updated keywords blanchet parents: 53219 diff changeset	73	"datatype_new_compat"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	74	"declaration"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	75	"declare"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	76	"def"
36455 30f96b4b108b updated keywords; wenzelm parents: 36356 diff changeset	77	"default_sort"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	78	"defer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	79	"defer_recdef"
18775 becdbf57eeb8 updated; wenzelm parents: 18757 diff changeset	80	"definition"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	81	"defs"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	82	"disable_pr"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	83	"display_drafts"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	84	"domain"
33840 f00a8956d6d0 updated keywords; wenzelm parents: 33687 diff changeset	85	"domain_isomorphism"
40585 e14bbfee8804 updated keywords haftmann parents: 40396 diff changeset	86	"domaindef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	87	"done"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	88	"enable_pr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	89	"end"
41530 c7e14c8088a6 updated keywords; wenzelm parents: 41435 diff changeset	90	"enriched_type"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	91	"equivariance"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	92	"exit"
24343 acc0f7aac619 updated keywords haftmann parents: 24249 diff changeset	93	"export_code"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	94	"extract"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	95	"extract_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	96	"finally"
29882 29154e67731d New command find_consts searching for constants by type (by Timothy Bourke). kleing parents: 29607 diff changeset	97	"find_consts"
17220 b41d8e290bf8 updated; wenzelm parents: 17147 diff changeset	98	"find_theorems"
46589 689311986778 adding new command "find_unused_assms" bulwahn parents: 45926 diff changeset	99	"find_unused_assms"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	100	"fix"
16231 91c0a3e253b1 add keywords fixrec and fixpat for HOLCF fixrec package huffman parents: 16168 diff changeset	101	"fixrec"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	102	"from"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	103	"full_prf"
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: 20453 diff changeset	104	"fun"
53637 f8147d885600 updated keywords krauss parents: 53553 diff changeset	105	"fun_cases"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	106	"function"
17850 6803625e71c4 updated; wenzelm parents: 17552 diff changeset	107	"guess"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	108	"have"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	109	"header"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	110	"help"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	111	"hence"
36180 2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	112	"hide_class"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	113	"hide_const"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	114	"hide_fact"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	115	"hide_type"
47262 87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	116	"import_const_map"
87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	117	"import_file"
46951 4e032ac36134 more precise TPTP keywords and dependencies; wenzelm parents: 46938 diff changeset	118	"import_tptp"
47262 87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	119	"import_type_map"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	120	"include"
12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	121	"including"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	122	"inductive"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	123	"inductive_cases"
23732 f9f89b7cfdc7 Adapted to changes in inductive definition package. berghofe parents: 22864 diff changeset	124	"inductive_set"
37734 489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation bulwahn parents: 37284 diff changeset	125	"inductive_simps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	126	"init_toplevel"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	127	"instance"
24437 c2a76e8a3d54 updated keywords haftmann parents: 24343 diff changeset	128	"instantiation"
15624 484178635bd8 Further work on interpretation commands. New command `interpret' for ballarin parents: 15598 diff changeset	129	"interpret"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	130	"interpretation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	131	"judgment"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	132	"kill"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	133	"kill_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	134	"lemma"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	135	"lemmas"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	136	"let"
47354 95846613e414 update keywords file huffman parents: 47308 diff changeset	137	"lift_definition"
53651 ee90c67502c9 restoring Transfer/Lifting context kuncar parents: 53637 diff changeset	138	"lifting_forget"
ee90c67502c9 restoring Transfer/Lifting context kuncar parents: 53637 diff changeset	139	"lifting_update"
27538 65f64da68a97 updated generated file; wenzelm parents: 27502 diff changeset	140	"linear_undo"
30463 f1cb00030d4f updated generated files; wenzelm parents: 29882 diff changeset	141	"local_setup"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	142	"locale"
49571 7e6fc0254d23 updated keywords; wenzelm parents: 49510 diff changeset	143	"locale_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	144	"method_setup"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	145	"moreover"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	146	"next"
33198 bfb9a790d1e7 updated keyword files to include "nitpick" and "nitpick_params" blanchet parents: 32804 diff changeset	147	"nitpick"
bfb9a790d1e7 updated keyword files to include "nitpick" and "nitpick_params" blanchet parents: 32804 diff changeset	148	"nitpick_params"
52623 fee0db8cf60d updated keywords; wenzelm parents: 52549 diff changeset	149	"no_adhoc_overloading"
24945 2c27817065bc updated; wenzelm parents: 24919 diff changeset	150	"no_notation"
15703 727ef1b8b3ee * empty log message * wenzelm parents: 15624 diff changeset	151	"no_syntax"
19255 e80e3fdda606 updated; wenzelm parents: 19149 diff changeset	152	"no_translations"
35414 cc8e4276d093 updated generated files; wenzelm parents: 35279 diff changeset	153	"no_type_notation"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	154	"nominal_datatype"
5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	155	"nominal_inductive"
28656 e92c79b3b154 Added nominal_inductive2. berghofe parents: 28482 diff changeset	156	"nominal_inductive2"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	157	"nominal_primrec"
41229 d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal'; wenzelm parents: 40970 diff changeset	158	"nonterminal"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	159	"notation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	160	"note"
40960 9e54eb514a46 formal notepad without any result; wenzelm parents: 40784 diff changeset	161	"notepad"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	162	"obtain"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	163	"oops"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	164	"oracle"
25516 ad25835675b9 updated haftmann parents: 25176 diff changeset	165	"overloading"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	166	"parse_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	167	"parse_translation"
40109 ebe2253e5c0e updated keywords; wenzelm parents: 39571 diff changeset	168	"partial_function"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	169	"pcpodef"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	170	"pr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	171	"prefer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	172	"presume"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	173	"pretty_setmargin"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	174	"prf"
53825 fb66852b3227 updated keywords blanchet parents: 53768 diff changeset	175	"primcorec"
53768 46a2154f250c updated keywords; wenzelm parents: 53651 diff changeset	176	"primcorecursive"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	177	"primrec"
53312 a1cf42366cea updated keywords blanchet parents: 53219 diff changeset	178	"primrec_new"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	179	"print_abbrevs"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	180	"print_antiquotations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	181	"print_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	182	"print_attributes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	183	"print_binds"
48981 3517d6f50b12 updated keywords blanchet parents: 48908 diff changeset	184	"print_bnfs"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	185	"print_bundles"
51691 69e3bc394f09 updated keywords; wenzelm parents: 51585 diff changeset	186	"print_case_translations"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	187	"print_cases"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	188	"print_claset"
20378 63a0aafc89ba updated code generator keywords haftmann parents: 20358 diff changeset	189	"print_classes"
31130 94cb206f8f6a updated keywords haftmann parents: 31108 diff changeset	190	"print_codeproc"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	191	"print_codesetup"
45061 39519609abe0 Include keywords print_coercions and print_coercion_maps berghofe parents: 44231 diff changeset	192	"print_coercions"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	193	"print_commands"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	194	"print_context"
51585 fcd5af4aac2b added 'print_defn_rules' command; wenzelm parents: 51381 diff changeset	195	"print_defn_rules"
41435 12585dfb86fe Diagnostic command to show locale dependencies. ballarin parents: 41249 diff changeset	196	"print_dependencies"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	197	"print_facts"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	198	"print_induct_rules"
50302 9149a07a6c67 added 'print_inductives' command; wenzelm parents: 50106 diff changeset	199	"print_inductives"
32804 ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps. ballarin parents: 31130 diff changeset	200	"print_interps"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	201	"print_locale"
c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	202	"print_locales"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	203	"print_methods"
52060 179236c82c2a renamed 'print_configs' to 'print_options'; wenzelm parents: 51836 diff changeset	204	"print_options"
24642 7865c239ba08 New diagnostic command print_orders. ballarin parents: 24437 diff changeset	205	"print_orders"
53219 ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned kuncar parents: 52984 diff changeset	206	"print_quot_maps"
35279 4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	207	"print_quotconsts"
4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	208	"print_quotients"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47267 diff changeset	209	"print_quotientsQ3"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47267 diff changeset	210	"print_quotmapsQ3"
12365 a90156701dad updated; wenzelm parents: 12342 diff changeset	211	"print_rules"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	212	"print_simpset"
52430 289e36c2870a proper diagnostic command 'print_state'; wenzelm parents: 52143 diff changeset	213	"print_state"
19272 5f376320109a updated; wenzelm parents: 19255 diff changeset	214	"print_statement"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	215	"print_syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	216	"print_theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	217	"print_theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	218	"print_trans_rules"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	219	"print_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	220	"proof"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	221	"prop"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	222	"pwd"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	223	"qed"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	224	"quickcheck"
45926 f4f22d87e364 added keywords bulwahn parents: 45193 diff changeset	225	"quickcheck_generator"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	226	"quickcheck_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	227	"quit"
35279 4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	228	"quotient_definition"
4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	229	"quotient_type"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	230	"realizability"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	231	"realizers"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	232	"recdef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	233	"recdef_tc"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	234	"record"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	235	"refute"
8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	236	"refute_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	237	"remove_thy"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	238	"rep_datatype"
36321 58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	239	"schematic_corollary"
58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	240	"schematic_lemma"
58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	241	"schematic_theorem"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	242	"sect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	243	"section"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	244	"setup"
47098 bab1c32c201e update etc/isar-keywords.el kuncar parents: 47069 diff changeset	245	"setup_lifting"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	246	"show"
22200 d4797b506752 updated; wenzelm parents: 22084 diff changeset	247	"simproc_setup"
53432 36ca6764027f updated keywords; wenzelm parents: 53312 diff changeset	248	"simps_of_case"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	249	"sledgehammer"
36114 e49fd7b1d932 updated keywords haftmann parents: 35414 diff changeset	250	"sledgehammer_params"
33898 2ca2693a8c10 include HOL-SMT keywords; wenzelm parents: 33874 diff changeset	251	"smt_status"
40117 ea388cb9bc57 updated keywords blanchet parents: 39571 diff changeset	252	"solve_direct"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	253	"sorry"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	254	"spark_end"
1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	255	"spark_open"
48908 713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files; wenzelm parents: 48867 diff changeset	256	"spark_open_siv"
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files; wenzelm parents: 48867 diff changeset	257	"spark_open_vcg"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	258	"spark_proof_functions"
1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	259	"spark_status"
42356 e8777e3ea6ef Added command for associating user-defined types with SPARK types. berghofe parents: 41564 diff changeset	260	"spark_types"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	261	"spark_vc"
14115 65ec3f73d00b Added package for definition by specification. skalberg parents: 14109 diff changeset	262	"specification"
25176 c5f80d70537e * empty log message * wenzelm parents: 25065 diff changeset	263	"statespace"
24919 ad3a8569759c updated keywords haftmann parents: 24912 diff changeset	264	"subclass"
28895 4e2914c2f8c5 Sublocale command. ballarin parents: 28721 diff changeset	265	"sublocale"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	266	"subsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	267	"subsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	268	"subsubsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	269	"subsubsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	270	"syntax"
40784 177e8cea3e09 added 'syntax_declaration' command; wenzelm parents: 40585 diff changeset	271	"syntax_declaration"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	272	"term"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	273	"termination"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	274	"text"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	275	"text_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	276	"then"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	277	"theorem"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	278	"theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	279	"theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	280	"thm"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	281	"thm_deps"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	282	"thus"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	283	"thy_deps"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	284	"translations"
38943 aea3d2566374 updated blanchet parents: 38837 diff changeset	285	"try"
46641 8801a24f9e9a renamed 'try_methods' to 'try0' blanchet parents: 46589 diff changeset	286	"try0"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	287	"txt"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	288	"txt_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	289	"typ"
35414 cc8e4276d093 updated generated files; wenzelm parents: 35279 diff changeset	290	"type_notation"
41249 26f12f98f50a Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature); wenzelm parents: 41229 diff changeset	291	"type_synonym"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	292	"typed_print_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	293	"typedecl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	294	"typedef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	295	"ultimately"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	296	"undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	297	"undos_proof"
18541 00890455e95f updated -- lost update!? wenzelm parents: 18520 diff changeset	298	"unfolding"
26184 64ee6a2ca6d6 Added unused_thms command. berghofe parents: 25577 diff changeset	299	"unused_thms"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	300	"use_thy"
12926 cd0dd6e0bf5c 'using' command; wenzelm parents: 12365 diff changeset	301	"using"
17552 744924bec974 Added new "value" command. berghofe parents: 17473 diff changeset	302	"value"
31130 94cb206f8f6a updated keywords haftmann parents: 31108 diff changeset	303	"values"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	304	"welcome"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	305	"with"
51789 75b92ff1d853 updated keywords blanchet parents: 51691 diff changeset	306	"wrap_free_constructors"
36505 79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable); wenzelm parents: 36472 diff changeset	307	"write"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	308	"{"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	309	"}"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	310
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	311	(defconst isar-keywords-minor
52143 36ffe23b25f8 syntax translations always depend on context; wenzelm parents: 52142 diff changeset	312	'("and"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	313	"assumes"
16771 2b534c5b5625 Added "attach" keyword for code generator setup. berghofe parents: 16701 diff changeset	314	"attach"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	315	"avoids"
15135 f00857c7539b Added "import" and "begin" nipkow parents: 14938 diff changeset	316	"begin"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	317	"binder"
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37785 diff changeset	318	"checking"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	319	"class_instance"
348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	320	"class_relation"
348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	321	"code_module"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	322	"congs"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	323	"constant"
16168 adb83939177f Locales: new element constrains, parameter renaming with syntax, ballarin parents: 16034 diff changeset	324	"constrains"
36472 3e677ca1e564 updated keywords haftmann parents: 36455 diff changeset	325	"datatypes"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	326	"defines"
17147 fa9e28b23d70 Adapted to new code generator syntax. berghofe parents: 17091 diff changeset	327	"file"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	328	"fixes"
19797 a527b3e1076a updated; wenzelm parents: 19655 diff changeset	329	"for"
36472 3e677ca1e564 updated keywords haftmann parents: 36455 diff changeset	330	"functions"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	331	"hints"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	332	"identifier"
19797 a527b3e1076a updated; wenzelm parents: 19655 diff changeset	333	"if"
15141 a95c2ff210ba import -> imports nipkow parents: 15135 diff changeset	334	"imports"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	335	"in"
47069 451fc10a81f3 more explicit Toplevel.open_target/close_target; wenzelm parents: 47066 diff changeset	336	"includes"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	337	"infix"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	338	"infixl"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	339	"infixr"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	340	"is"
46938 cda018294515 some support for outer syntax keyword declarations within theory header; wenzelm parents: 46641 diff changeset	341	"keywords"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	342	"lazy"
24249 1f60b45c5f97 renamed keyword "to" to "module_name" haftmann parents: 24120 diff changeset	343	"module_name"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	344	"monos"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	345	"morphisms"
52984 2ab38527aca7 updated keywords; wenzelm parents: 52623 diff changeset	346	"no_discs_sels"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	347	"notes"
18888 3b643f81b378 updated; wenzelm parents: 18775 diff changeset	348	"obtains"
13364 d3c7d05d8839 updated; wenzelm parents: 12954 diff changeset	349	"open"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	350	"output"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	351	"overloaded"
51381 4d691437c076 updated keywords (cf. 84d01fd733cf); wenzelm parents: 51313 diff changeset	352	"parametric"
11618 7067101463c0 updated; wenzelm parents: 11538 diff changeset	353	"permissive"
33685 29106208ccf7 updated keywords; wenzelm parents: 33198 diff changeset	354	"pervasive"
50106 e12e4ad93183 updated keywords; wenzelm parents: 49640 diff changeset	355	"rep_compat"
12935 d697091d1591 updated; wenzelm parents: 12926 diff changeset	356	"shows"
12042 1e5c01d5fe04 updated; wenzelm parents: 12040 diff changeset	357	"structure"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	358	"type_class"
348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	359	"type_constructor"
19633 a6fad1e8bbd2 updated; wenzelm parents: 19564 diff changeset	360	"unchecked"
40386 bdce9a9ec0cd updated keywords; wenzelm parents: 40209 diff changeset	361	"unsafe"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	362	"where"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	363
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	364	(defconst isar-keywords-control
25577 d739f48ef40c updated; wenzelm parents: 25516 diff changeset	365	'("Isabelle\\.command"
d739f48ef40c updated; wenzelm parents: 25516 diff changeset	366	"ProofGeneral\\.inform_file_processed"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	367	"ProofGeneral\\.inform_file_retracted"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	368	"ProofGeneral\\.kill_proof"
52437 c88354589b43 more formal ProofGeneral command setup within theory Pure; wenzelm parents: 52432 diff changeset	369	"ProofGeneral\\.pr"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	370	"ProofGeneral\\.process_pgip"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	371	"ProofGeneral\\.restart"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	372	"ProofGeneral\\.undo"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	373	"cannot_undo"
40396 c4c6fa6819aa updated keywords; wenzelm parents: 40386 diff changeset	374	"cd"
c4c6fa6819aa updated keywords; wenzelm parents: 40386 diff changeset	375	"commit"
37987 aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	376	"disable_pr"
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	377	"enable_pr"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	378	"exit"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	379	"init_toplevel"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	380	"kill"
37987 aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	381	"kill_thy"
27538 65f64da68a97 updated generated file; wenzelm parents: 27502 diff changeset	382	"linear_undo"
51270 17d30843fc3b reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy; wenzelm parents: 50302 diff changeset	383	"pretty_setmargin"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	384	"quit"
37987 aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	385	"remove_thy"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	386	"undo"
37987 aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	387	"undos_proof"
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents; wenzelm parents: 37983 diff changeset	388	"use_thy"))
11538 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-diag
26482 e7f677b85bfd updated generated file; wenzelm parents: 26394 diff changeset	391	'("ML_command"
26394 ddd7825ea4cd * empty log message * wenzelm parents: 26184 diff changeset	392	"ML_val"
20568 9b7f59c1bdfc updated; wenzelm parents: 20523 diff changeset	393	"class_deps"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	394	"code_deps"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	395	"code_thms"
14938 393b75c92c07 updated; wenzelm parents: 14660 diff changeset	396	"display_drafts"
29882 29154e67731d New command find_consts searching for constants by type (by Timothy Bourke). kleing parents: 29607 diff changeset	397	"find_consts"
17220 b41d8e290bf8 updated; wenzelm parents: 17147 diff changeset	398	"find_theorems"
46589 689311986778 adding new command "find_unused_assms" bulwahn parents: 45926 diff changeset	399	"find_unused_assms"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	400	"full_prf"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	401	"header"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	402	"help"
49571 7e6fc0254d23 updated keywords; wenzelm parents: 49510 diff changeset	403	"locale_deps"
33198 bfb9a790d1e7 updated keyword files to include "nitpick" and "nitpick_params" blanchet parents: 32804 diff changeset	404	"nitpick"
52438 7b5a5116f3af back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means; wenzelm parents: 52437 diff changeset	405	"pr"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	406	"prf"
21732 4d4cde714500 updated; wenzelm parents: 21302 diff changeset	407	"print_abbrevs"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	408	"print_antiquotations"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	409	"print_attributes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	410	"print_binds"
48981 3517d6f50b12 updated keywords blanchet parents: 48908 diff changeset	411	"print_bnfs"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	412	"print_bundles"
51691 69e3bc394f09 updated keywords; wenzelm parents: 51585 diff changeset	413	"print_case_translations"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	414	"print_cases"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	415	"print_claset"
20378 63a0aafc89ba updated code generator keywords haftmann parents: 20358 diff changeset	416	"print_classes"
31130 94cb206f8f6a updated keywords haftmann parents: 31108 diff changeset	417	"print_codeproc"
22288 c565f33ec70f updated keywords haftmann parents: 22200 diff changeset	418	"print_codesetup"
45061 39519609abe0 Include keywords print_coercions and print_coercion_maps berghofe parents: 44231 diff changeset	419	"print_coercions"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	420	"print_commands"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	421	"print_context"
51585 fcd5af4aac2b added 'print_defn_rules' command; wenzelm parents: 51381 diff changeset	422	"print_defn_rules"
41435 12585dfb86fe Diagnostic command to show locale dependencies. ballarin parents: 41249 diff changeset	423	"print_dependencies"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	424	"print_facts"
11661 37cfa9aad9c0 updated; wenzelm parents: 11618 diff changeset	425	"print_induct_rules"
50302 9149a07a6c67 added 'print_inductives' command; wenzelm parents: 50106 diff changeset	426	"print_inductives"
32804 ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps. ballarin parents: 31130 diff changeset	427	"print_interps"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	428	"print_locale"
c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	429	"print_locales"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	430	"print_methods"
52060 179236c82c2a renamed 'print_configs' to 'print_options'; wenzelm parents: 51836 diff changeset	431	"print_options"
24642 7865c239ba08 New diagnostic command print_orders. ballarin parents: 24437 diff changeset	432	"print_orders"
53219 ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned kuncar parents: 52984 diff changeset	433	"print_quot_maps"
35279 4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	434	"print_quotconsts"
4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	435	"print_quotients"
47308 9caab698dbe4 new package Lifting - initial commit kuncar parents: 47267 diff changeset	436	"print_quotientsQ3"
9caab698dbe4 new package Lifting - initial commit kuncar parents: 47267 diff changeset	437	"print_quotmapsQ3"
12365 a90156701dad updated; wenzelm parents: 12342 diff changeset	438	"print_rules"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	439	"print_simpset"
52430 289e36c2870a proper diagnostic command 'print_state'; wenzelm parents: 52143 diff changeset	440	"print_state"
19272 5f376320109a updated; wenzelm parents: 19255 diff changeset	441	"print_statement"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	442	"print_syntax"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	443	"print_theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	444	"print_theory"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	445	"print_trans_rules"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	446	"prop"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	447	"pwd"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	448	"quickcheck"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	449	"refute"
22864 e2511e6e5cbb updated; wenzelm parents: 22486 diff changeset	450	"sledgehammer"
33898 2ca2693a8c10 include HOL-SMT keywords; wenzelm parents: 33874 diff changeset	451	"smt_status"
40117 ea388cb9bc57 updated keywords blanchet parents: 39571 diff changeset	452	"solve_direct"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	453	"spark_status"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	454	"term"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	455	"thm"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	456	"thm_deps"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	457	"thy_deps"
38943 aea3d2566374 updated blanchet parents: 38837 diff changeset	458	"try"
46641 8801a24f9e9a renamed 'try_methods' to 'try0' blanchet parents: 46589 diff changeset	459	"try0"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	460	"typ"
26184 64ee6a2ca6d6 Added unused_thms command. berghofe parents: 25577 diff changeset	461	"unused_thms"
17552 744924bec974 Added new "value" command. berghofe parents: 17473 diff changeset	462	"value"
31130 94cb206f8f6a updated keywords haftmann parents: 31108 diff changeset	463	"values"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	464	"welcome"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	465
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	466	(defconst isar-keywords-theory-begin
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	467	'("theory"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	468
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	469	(defconst isar-keywords-theory-switch
21302 4c8f3dfc7124 updated; wenzelm parents: 21203 diff changeset	470	'())
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	471
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	472	(defconst isar-keywords-theory-end
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	473	'("end"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	474
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	475	(defconst isar-keywords-theory-heading
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	476	'("chapter"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	477	"section"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	478	"subsection"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	479	"subsubsection"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	480
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	481	(defconst isar-keywords-theory-decl
26482 e7f677b85bfd updated generated file; wenzelm parents: 26394 diff changeset	482	'("ML"
48867 e9beabf045ab some support for inlining file content into outer syntax token language; wenzelm parents: 48709 diff changeset	483	"ML_file"
19069 a4b956f8b233 updated; wenzelm parents: 18888 diff changeset	484	"abbreviation"
52623 fee0db8cf60d updated keywords; wenzelm parents: 52549 diff changeset	485	"adhoc_overloading"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	486	"arities"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	487	"atom_decl"
30527 fae488569faf updated generated files; wenzelm parents: 30463 diff changeset	488	"attribute_setup"
18612 7300f75028dc updated; wenzelm parents: 18552 diff changeset	489	"axiomatization"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	490	"bundle"
53432 36ca6764027f updated keywords; wenzelm parents: 53312 diff changeset	491	"case_of_simps"
18552 30911da9fb27 class now a keyword haftmann parents: 18541 diff changeset	492	"class"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	493	"classes"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	494	"classrel"
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51789 diff changeset	495	"codatatype"
27102 a98cd7450204 updated haftmann parents: 26896 diff changeset	496	"code_abort"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	497	"code_class"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	498	"code_const"
22486 d3b6cb2306b6 updated keywords haftmann parents: 22288 diff changeset	499	"code_datatype"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	500	"code_identifier"
24997 730d74336b4d updated haftmann parents: 24945 diff changeset	501	"code_include"
20424 d5b4b55ad277 updated keywords haftmann parents: 20378 diff changeset	502	"code_instance"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	503	"code_modulename"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	504	"code_monad"
52142 348aed032cda updated keywords; wenzelm parents: 52060 diff changeset	505	"code_printing"
36472 3e677ca1e564 updated keywords haftmann parents: 36455 diff changeset	506	"code_reflect"
21028 ed94ba513989 updated; wenzelm parents: 21027 diff changeset	507	"code_reserved"
20453 855f07fabd76 final syntax for some Isar code generator keywords haftmann parents: 20424 diff changeset	508	"code_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	509	"coinductive"
23732 f9f89b7cfdc7 Adapted to changes in inductive definition package. berghofe parents: 22864 diff changeset	510	"coinductive_set"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	511	"consts"
21302 4c8f3dfc7124 updated; wenzelm parents: 21203 diff changeset	512	"context"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	513	"datatype"
51804 be6e703908f4 renamed BNF "(co)data" commands to names that are closer to their final names blanchet parents: 51789 diff changeset	514	"datatype_new"
53312 a1cf42366cea updated keywords blanchet parents: 53219 diff changeset	515	"datatype_new_compat"
22084 2fef69700f50 updated wenzelm parents: 21806 diff changeset	516	"declaration"
23804 5801141870b1 updated; wenzelm parents: 23732 diff changeset	517	"declare"
36455 30f96b4b108b updated keywords; wenzelm parents: 36356 diff changeset	518	"default_sort"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	519	"defer_recdef"
18775 becdbf57eeb8 updated; wenzelm parents: 18757 diff changeset	520	"definition"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	521	"defs"
12040 61e99f0f5c01 updated; wenzelm parents: 11746 diff changeset	522	"domain"
33840 f00a8956d6d0 updated keywords; wenzelm parents: 33687 diff changeset	523	"domain_isomorphism"
40585 e14bbfee8804 updated keywords haftmann parents: 40396 diff changeset	524	"domaindef"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	525	"equivariance"
51275 3928173409e4 reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system; wenzelm parents: 51270 diff changeset	526	"export_code"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	527	"extract"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	528	"extract_type"
16231 91c0a3e253b1 add keywords fixrec and fixpat for HOLCF fixrec package huffman parents: 16168 diff changeset	529	"fixrec"
20523 36a59e5d0039 Major update to function package, including new syntax and the (only theoretical) krauss parents: 20453 diff changeset	530	"fun"
53637 f8147d885600 updated keywords krauss parents: 53553 diff changeset	531	"fun_cases"
36180 2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	532	"hide_class"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	533	"hide_const"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	534	"hide_fact"
2db3711b2b03 updated keywords; wenzelm parents: 36114 diff changeset	535	"hide_type"
47262 87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	536	"import_const_map"
87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	537	"import_file"
46951 4e032ac36134 more precise TPTP keywords and dependencies; wenzelm parents: 46938 diff changeset	538	"import_tptp"
47262 87ba9d3e1020 more keywords; wenzelm parents: 47098 diff changeset	539	"import_type_map"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	540	"inductive"
23732 f9f89b7cfdc7 Adapted to changes in inductive definition package. berghofe parents: 22864 diff changeset	541	"inductive_set"
24437 c2a76e8a3d54 updated keywords haftmann parents: 24343 diff changeset	542	"instantiation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	543	"judgment"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	544	"lemmas"
53651 ee90c67502c9 restoring Transfer/Lifting context kuncar parents: 53637 diff changeset	545	"lifting_forget"
ee90c67502c9 restoring Transfer/Lifting context kuncar parents: 53637 diff changeset	546	"lifting_update"
30463 f1cb00030d4f updated generated files; wenzelm parents: 29882 diff changeset	547	"local_setup"
12059 c224c941769f added "locale", "print_locale", "print_locales"; wenzelm parents: 12042 diff changeset	548	"locale"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	549	"method_setup"
33198 bfb9a790d1e7 updated keyword files to include "nitpick" and "nitpick_params" blanchet parents: 32804 diff changeset	550	"nitpick_params"
52623 fee0db8cf60d updated keywords; wenzelm parents: 52549 diff changeset	551	"no_adhoc_overloading"
24945 2c27817065bc updated; wenzelm parents: 24919 diff changeset	552	"no_notation"
15703 727ef1b8b3ee * empty log message * wenzelm parents: 15624 diff changeset	553	"no_syntax"
19255 e80e3fdda606 updated; wenzelm parents: 19149 diff changeset	554	"no_translations"
35414 cc8e4276d093 updated generated files; wenzelm parents: 35279 diff changeset	555	"no_type_notation"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	556	"nominal_datatype"
41229 d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal'; wenzelm parents: 40970 diff changeset	557	"nonterminal"
21203 8154a62bb498 updated; wenzelm parents: 21057 diff changeset	558	"notation"
40960 9e54eb514a46 formal notepad without any result; wenzelm parents: 40784 diff changeset	559	"notepad"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	560	"oracle"
25516 ad25835675b9 updated haftmann parents: 25176 diff changeset	561	"overloading"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	562	"parse_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	563	"parse_translation"
40209 8ec474f94d61 regenerated keyword file krauss parents: 40119 diff changeset	564	"partial_function"
53825 fb66852b3227 updated keywords blanchet parents: 53768 diff changeset	565	"primcorec"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	566	"primrec"
53312 a1cf42366cea updated keywords blanchet parents: 53219 diff changeset	567	"primrec_new"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	568	"print_ast_translation"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	569	"print_translation"
45926 f4f22d87e364 added keywords bulwahn parents: 45193 diff changeset	570	"quickcheck_generator"
14109 7aa5b79daffb Added keywords for random testing. berghofe parents: 13802 diff changeset	571	"quickcheck_params"
13407 d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	572	"realizability"
d128b5915f6b Added program extraction keywords. berghofe parents: 13364 diff changeset	573	"realizers"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	574	"recdef"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	575	"record"
14349 8d92e426eb38 'refute', 'refute_params'. webertj parents: 14223 diff changeset	576	"refute_params"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	577	"setup"
47098 bab1c32c201e update etc/isar-keywords.el kuncar parents: 47069 diff changeset	578	"setup_lifting"
22200 d4797b506752 updated; wenzelm parents: 22084 diff changeset	579	"simproc_setup"
53432 36ca6764027f updated keywords; wenzelm parents: 53312 diff changeset	580	"simps_of_case"
36114 e49fd7b1d932 updated keywords haftmann parents: 35414 diff changeset	581	"sledgehammer_params"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	582	"spark_end"
1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	583	"spark_open"
48908 713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files; wenzelm parents: 48867 diff changeset	584	"spark_open_siv"
713f24d7a40f added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files; wenzelm parents: 48867 diff changeset	585	"spark_open_vcg"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	586	"spark_proof_functions"
42356 e8777e3ea6ef Added command for associating user-defined types with SPARK types. berghofe parents: 41564 diff changeset	587	"spark_types"
25176 c5f80d70537e * empty log message * wenzelm parents: 25065 diff changeset	588	"statespace"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	589	"syntax"
40784 177e8cea3e09 added 'syntax_declaration' command; wenzelm parents: 40585 diff changeset	590	"syntax_declaration"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	591	"text"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	592	"text_raw"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	593	"theorems"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	594	"translations"
35414 cc8e4276d093 updated generated files; wenzelm parents: 35279 diff changeset	595	"type_notation"
41249 26f12f98f50a Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature); wenzelm parents: 41229 diff changeset	596	"type_synonym"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	597	"typed_print_translation"
51295 71fc3776c453 discontinued redundant 'use' command; wenzelm parents: 51293 diff changeset	598	"typedecl"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	599
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	600	(defconst isar-keywords-theory-script
37734 489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation bulwahn parents: 37284 diff changeset	601	'("inductive_cases"
489ac1ecb9f1 added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation bulwahn parents: 37284 diff changeset	602	"inductive_simps"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	603
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	604	(defconst isar-keywords-theory-goal
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	605	'("ax_specification"
51836 4d6dcd51dd52 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration) blanchet parents: 51804 diff changeset	606	"bnf"
31106 9a1178204dc0 Added pred_code command bulwahn parents: 30856 diff changeset	607	"code_pred"
14223 0ee05eef881b Added support for making constants final, that is, ensuring that no skalberg parents: 14115 diff changeset	608	"corollary"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	609	"cpodef"
41530 c7e14c8088a6 updated keywords; wenzelm parents: 41435 diff changeset	610	"enriched_type"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	611	"function"
11746 9bf11f1de9d6 updated; wenzelm parents: 11661 diff changeset	612	"instance"
15598 4ab52355bb53 Registrations of global locale interpretations: improved, better naming. ballarin parents: 15596 diff changeset	613	"interpretation"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	614	"lemma"
47354 95846613e414 update keywords file huffman parents: 47308 diff changeset	615	"lift_definition"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	616	"nominal_inductive"
28656 e92c79b3b154 Added nominal_inductive2. berghofe parents: 28482 diff changeset	617	"nominal_inductive2"
24904 5b59fadfe878 updated; wenzelm parents: 24876 diff changeset	618	"nominal_primrec"
16701 abd0abd66387 add keywords cpodef, pcpodef (for HOLCF) huffman parents: 16419 diff changeset	619	"pcpodef"
53768 46a2154f250c updated keywords; wenzelm parents: 53651 diff changeset	620	"primcorecursive"
47098 bab1c32c201e update etc/isar-keywords.el kuncar parents: 47069 diff changeset	621	"quotient_definition"
35279 4f6760122b2a update the keywords files Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35223 diff changeset	622	"quotient_type"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	623	"recdef_tc"
27102 a98cd7450204 updated haftmann parents: 26896 diff changeset	624	"rep_datatype"
36321 58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	625	"schematic_corollary"
58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	626	"schematic_lemma"
58d4dc6000fc updated generated files; wenzelm parents: 36180 diff changeset	627	"schematic_theorem"
41564 1cbf33a4406a Include HOL-SPARK keywords berghofe parents: 41530 diff changeset	628	"spark_vc"
14115 65ec3f73d00b Added package for definition by specification. skalberg parents: 14109 diff changeset	629	"specification"
24919 ad3a8569759c updated keywords haftmann parents: 24912 diff changeset	630	"subclass"
28895 4e2914c2f8c5 Sublocale command. ballarin parents: 28721 diff changeset	631	"sublocale"
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19272 diff changeset	632	"termination"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	633	"theorem"
49074 d8af889dcbe3 renamed three BNF/(co)datatype-related commands blanchet parents: 49020 diff changeset	634	"typedef"
51789 75b92ff1d853 updated keywords blanchet parents: 51691 diff changeset	635	"wrap_free_constructors"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	636
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	637	(defconst isar-keywords-qed
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	638	'("\\."
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	639	"\\.\\."
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	640	"by"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	641	"done"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	642	"sorry"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	643
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	644	(defconst isar-keywords-qed-block
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	645	'("qed"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	646
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	647	(defconst isar-keywords-qed-global
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	648	'("oops"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	649
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	650	(defconst isar-keywords-proof-heading
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	651	'("sect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	652	"subsect"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	653	"subsubsect"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	654
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	655	(defconst isar-keywords-proof-goal
29607 2db3537c3535 updated generated files; wenzelm parents: 29252 diff changeset	656	'("have"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	657	"hence"
29607 2db3537c3535 updated generated files; wenzelm parents: 29252 diff changeset	658	"interpret"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	659
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	660	(defconst isar-keywords-proof-block
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	661	'("next"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	662	"proof"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	663
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	664	(defconst isar-keywords-proof-open
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	665	'("{"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	666
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	667	(defconst isar-keywords-proof-close
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	668	'("}"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	669
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	670	(defconst isar-keywords-proof-chain
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	671	'("finally"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	672	"from"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	673	"then"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	674	"ultimately"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	675	"with"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	676
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	677	(defconst isar-keywords-proof-decl
28280 fd0485db7d5a updated generated file; wenzelm parents: 27621 diff changeset	678	'("ML_prf"
fd0485db7d5a updated generated file; wenzelm parents: 27621 diff changeset	679	"also"
47057 12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	680	"include"
12423b36fcc4 basic support for bundled declarations; wenzelm parents: 46974 diff changeset	681	"including"
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	682	"let"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	683	"moreover"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	684	"note"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	685	"txt"
12926 cd0dd6e0bf5c 'using' command; wenzelm parents: 12365 diff changeset	686	"txt_raw"
18541 00890455e95f updated -- lost update!? wenzelm parents: 18520 diff changeset	687	"unfolding"
36505 79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable); wenzelm parents: 36472 diff changeset	688	"using"
79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable); wenzelm parents: 36472 diff changeset	689	"write"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	690
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	691	(defconst isar-keywords-proof-asm
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	692	'("assume"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	693	"case"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	694	"def"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	695	"fix"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	696	"presume"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	697
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	698	(defconst isar-keywords-proof-asm-goal
17850 6803625e71c4 updated; wenzelm parents: 17552 diff changeset	699	'("guess"
21806 6086783d4214 updated; wenzelm parents: 21732 diff changeset	700	"obtain"
6086783d4214 updated; wenzelm parents: 21732 diff changeset	701	"show"
6086783d4214 updated; wenzelm parents: 21732 diff changeset	702	"thus"))
11538 f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	703
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	704	(defconst isar-keywords-proof-script
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	705	'("apply"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	706	"apply_end"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	707	"back"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	708	"defer"
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	709	"prefer"))
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	710
f8588786cc9c keyword classification tables for Isabelle/Isar Proof General wenzelm parents: diff changeset	711	(provide 'isar-keywords)

author	blanchet
	Tue, 24 Sep 2013 16:54:50 +0200
changeset 53825	fb66852b3227
parent 53768	46a2154f250c
child 54447	019394de2b41
permissions	-rw-r--r--