wneuper/isa: etc/isar-keywords.el@9b062fef2c91 (annotated)

wenzelm@11538	1	;;
wenzelm@11538	2	;; Keyword classification tables for Isabelle/Isar.
blanchet@50525	3	;; Generated from HOLCF + HOL-BNF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
wenzelm@24904	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
wenzelm@11538	5	;;
wenzelm@11538	6
wenzelm@11538	7	(defconst isar-keywords-major
wenzelm@11538	8	'("\\."
wenzelm@15762	9	"\\.\\."
wenzelm@25577	10	"Isabelle\\.command"
wenzelm@11538	11	"ML"
wenzelm@11538	12	"ML_command"
wenzelm@49882	13	"ML_file"
wenzelm@28280	14	"ML_prf"
wenzelm@26394	15	"ML_val"
wenzelm@11538	16	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	17	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	18	"ProofGeneral\\.kill_proof"
wenzelm@33874	19	"ProofGeneral\\.pr"
wenzelm@14938	20	"ProofGeneral\\.process_pgip"
wenzelm@11538	21	"ProofGeneral\\.restart"
wenzelm@11538	22	"ProofGeneral\\.undo"
wenzelm@19069	23	"abbreviation"
wenzelm@11538	24	"also"
wenzelm@11538	25	"apply"
wenzelm@11538	26	"apply_end"
wenzelm@11538	27	"arities"
wenzelm@11538	28	"assume"
wenzelm@24904	29	"atom_decl"
wenzelm@30529	30	"attribute_setup"
skalberg@14223	31	"ax_specification"
wenzelm@18612	32	"axiomatization"
wenzelm@11538	33	"axioms"
wenzelm@11538	34	"back"
blanchet@49996	35	"bnf_def"
wenzelm@33687	36	"boogie_end"
wenzelm@33687	37	"boogie_open"
wenzelm@33687	38	"boogie_status"
wenzelm@33687	39	"boogie_vc"
wenzelm@47928	40	"bundle"
wenzelm@11538	41	"by"
wenzelm@11538	42	"cannot_undo"
wenzelm@11538	43	"case"
wenzelm@11538	44	"cd"
wenzelm@11538	45	"chapter"
haftmann@18552	46	"class"
wenzelm@20568	47	"class_deps"
wenzelm@11538	48	"classes"
wenzelm@11538	49	"classrel"
blanchet@50127	50	"codata"
haftmann@27102	51	"code_abort"
haftmann@20424	52	"code_class"
haftmann@20453	53	"code_const"
haftmann@22486	54	"code_datatype"
wenzelm@22864	55	"code_deps"
haftmann@24997	56	"code_include"
haftmann@20424	57	"code_instance"
wenzelm@21203	58	"code_modulename"
wenzelm@22084	59	"code_monad"
bulwahn@31106	60	"code_pred"
haftmann@36468	61	"code_reflect"
wenzelm@21028	62	"code_reserved"
haftmann@22288	63	"code_thms"
haftmann@20453	64	"code_type"
wenzelm@11538	65	"coinductive"
berghofe@23732	66	"coinductive_set"
wenzelm@11538	67	"commit"
wenzelm@11538	68	"consts"
wenzelm@11538	69	"context"
wenzelm@11746	70	"corollary"
huffman@16701	71	"cpodef"
blanchet@50127	72	"data"
wenzelm@11538	73	"datatype"
wenzelm@22084	74	"declaration"
wenzelm@11538	75	"declare"
wenzelm@11538	76	"def"
wenzelm@36455	77	"default_sort"
wenzelm@11538	78	"defer"
wenzelm@11538	79	"defer_recdef"
wenzelm@18775	80	"definition"
wenzelm@11538	81	"defs"
wenzelm@11538	82	"disable_pr"
wenzelm@14938	83	"display_drafts"
wenzelm@12040	84	"domain"
wenzelm@33840	85	"domain_isomorphism"
haftmann@40822	86	"domaindef"
wenzelm@11538	87	"done"
wenzelm@11538	88	"enable_pr"
wenzelm@11538	89	"end"
wenzelm@41778	90	"enriched_type"
wenzelm@24904	91	"equivariance"
wenzelm@11538	92	"exit"
haftmann@24343	93	"export_code"
berghofe@13407	94	"extract"
berghofe@13407	95	"extract_type"
wenzelm@11538	96	"finally"
kleing@29819	97	"find_consts"
wenzelm@17220	98	"find_theorems"
bulwahn@47460	99	"find_unused_assms"
wenzelm@11538	100	"fix"
huffman@16231	101	"fixrec"
wenzelm@11538	102	"from"
wenzelm@11538	103	"full_prf"
krauss@20523	104	"fun"
krauss@19564	105	"function"
wenzelm@17850	106	"guess"
wenzelm@11538	107	"have"
wenzelm@11538	108	"header"
wenzelm@21732	109	"help"
wenzelm@11538	110	"hence"
wenzelm@36180	111	"hide_class"
wenzelm@36180	112	"hide_const"
wenzelm@36180	113	"hide_fact"
wenzelm@36180	114	"hide_type"
wenzelm@48133	115	"import_const_map"
wenzelm@48133	116	"import_file"
wenzelm@47825	117	"import_tptp"
wenzelm@48133	118	"import_type_map"
wenzelm@47928	119	"include"
wenzelm@47928	120	"including"
wenzelm@11538	121	"inductive"
wenzelm@11538	122	"inductive_cases"
berghofe@23732	123	"inductive_set"
bulwahn@37733	124	"inductive_simps"
wenzelm@11538	125	"init_toplevel"
wenzelm@11538	126	"instance"
haftmann@24437	127	"instantiation"
ballarin@15624	128	"interpret"
ballarin@15598	129	"interpretation"
wenzelm@11538	130	"judgment"
wenzelm@11538	131	"kill"
wenzelm@11538	132	"kill_thy"
wenzelm@11538	133	"lemma"
wenzelm@11538	134	"lemmas"
wenzelm@11538	135	"let"
huffman@48212	136	"lift_definition"
wenzelm@27538	137	"linear_undo"
wenzelm@30463	138	"local_setup"
wenzelm@12059	139	"locale"
wenzelm@50586	140	"locale_deps"
wenzelm@11538	141	"method_setup"
wenzelm@11538	142	"moreover"
wenzelm@11538	143	"next"
blanchet@33198	144	"nitpick"
blanchet@33198	145	"nitpick_params"
wenzelm@24945	146	"no_notation"
wenzelm@15703	147	"no_syntax"
wenzelm@19255	148	"no_translations"
wenzelm@35419	149	"no_type_notation"
wenzelm@24904	150	"nominal_datatype"
wenzelm@24904	151	"nominal_inductive"
berghofe@28656	152	"nominal_inductive2"
wenzelm@24904	153	"nominal_primrec"
wenzelm@41495	154	"nonterminal"
wenzelm@21203	155	"notation"
wenzelm@11538	156	"note"
wenzelm@41208	157	"notepad"
wenzelm@11538	158	"obtain"
wenzelm@11538	159	"oops"
wenzelm@11538	160	"oracle"
haftmann@25516	161	"overloading"
wenzelm@11538	162	"parse_ast_translation"
wenzelm@11538	163	"parse_translation"
haftmann@40356	164	"partial_function"
huffman@16701	165	"pcpodef"
wenzelm@11538	166	"pr"
wenzelm@11538	167	"prefer"
wenzelm@11538	168	"presume"
wenzelm@11538	169	"pretty_setmargin"
wenzelm@11538	170	"prf"
wenzelm@11538	171	"primrec"
wenzelm@21732	172	"print_abbrevs"
wenzelm@11538	173	"print_antiquotations"
wenzelm@11538	174	"print_ast_translation"
wenzelm@11538	175	"print_attributes"
wenzelm@11538	176	"print_binds"
blanchet@49996	177	"print_bnfs"
wenzelm@47928	178	"print_bundles"
wenzelm@11538	179	"print_cases"
wenzelm@11538	180	"print_claset"
haftmann@20378	181	"print_classes"
haftmann@31130	182	"print_codeproc"
haftmann@22288	183	"print_codesetup"
berghofe@45927	184	"print_coercion_maps"
berghofe@45927	185	"print_coercions"
wenzelm@11538	186	"print_commands"
wenzelm@24120	187	"print_configs"
wenzelm@11538	188	"print_context"
ballarin@41683	189	"print_dependencies"
wenzelm@14938	190	"print_drafts"
wenzelm@11538	191	"print_facts"
wenzelm@11661	192	"print_induct_rules"
wenzelm@51317	193	"print_inductives"
ballarin@32788	194	"print_interps"
wenzelm@12059	195	"print_locale"
wenzelm@12059	196	"print_locales"
wenzelm@11538	197	"print_methods"
ballarin@24642	198	"print_orders"
kaliszyk@35279	199	"print_quotconsts"
kaliszyk@35279	200	"print_quotients"
kuncar@48153	201	"print_quotientsQ3"
kaliszyk@35279	202	"print_quotmaps"
kuncar@48153	203	"print_quotmapsQ3"
wenzelm@12365	204	"print_rules"
wenzelm@11538	205	"print_simpset"
wenzelm@19272	206	"print_statement"
wenzelm@11538	207	"print_syntax"
wenzelm@11538	208	"print_theorems"
wenzelm@11538	209	"print_theory"
wenzelm@11538	210	"print_trans_rules"
wenzelm@11538	211	"print_translation"
wenzelm@11538	212	"proof"
wenzelm@11538	213	"prop"
wenzelm@11538	214	"pwd"
wenzelm@11538	215	"qed"
berghofe@14109	216	"quickcheck"
bulwahn@46797	217	"quickcheck_generator"
berghofe@14109	218	"quickcheck_params"
wenzelm@11538	219	"quit"
kaliszyk@35279	220	"quotient_definition"
kaliszyk@35279	221	"quotient_type"
berghofe@13407	222	"realizability"
berghofe@13407	223	"realizers"
wenzelm@11538	224	"recdef"
wenzelm@11538	225	"recdef_tc"
wenzelm@11538	226	"record"
webertj@14349	227	"refute"
webertj@14349	228	"refute_params"
wenzelm@11538	229	"remove_thy"
wenzelm@11538	230	"rep_datatype"
wenzelm@36321	231	"schematic_corollary"
wenzelm@36321	232	"schematic_lemma"
wenzelm@36321	233	"schematic_theorem"
wenzelm@11538	234	"sect"
wenzelm@11538	235	"section"
wenzelm@11538	236	"setup"
kuncar@47968	237	"setup_lifting"
wenzelm@11538	238	"show"
wenzelm@22200	239	"simproc_setup"
wenzelm@22864	240	"sledgehammer"
haftmann@36114	241	"sledgehammer_params"
wenzelm@33898	242	"smt_status"
blanchet@40361	243	"solve_direct"
wenzelm@11538	244	"sorry"
berghofe@41812	245	"spark_end"
berghofe@41812	246	"spark_open"
wenzelm@49923	247	"spark_open_siv"
wenzelm@49923	248	"spark_open_vcg"
berghofe@41812	249	"spark_proof_functions"
berghofe@41812	250	"spark_status"
berghofe@43227	251	"spark_types"
berghofe@41812	252	"spark_vc"
skalberg@14115	253	"specification"
wenzelm@25176	254	"statespace"
haftmann@24919	255	"subclass"
ballarin@28895	256	"sublocale"
wenzelm@11538	257	"subsect"
wenzelm@11538	258	"subsection"
wenzelm@11538	259	"subsubsect"
wenzelm@11538	260	"subsubsection"
wenzelm@11538	261	"syntax"
wenzelm@41034	262	"syntax_declaration"
wenzelm@11538	263	"term"
krauss@19564	264	"termination"
wenzelm@11538	265	"text"
wenzelm@11538	266	"text_raw"
wenzelm@11538	267	"then"
wenzelm@11538	268	"theorem"
wenzelm@11538	269	"theorems"
wenzelm@11538	270	"theory"
wenzelm@11538	271	"thm"
wenzelm@11538	272	"thm_deps"
wenzelm@11538	273	"thus"
haftmann@22486	274	"thy_deps"
wenzelm@11538	275	"translations"
blanchet@39169	276	"try"
blanchet@47512	277	"try0"
wenzelm@11538	278	"txt"
wenzelm@11538	279	"txt_raw"
wenzelm@11538	280	"typ"
wenzelm@35419	281	"type_notation"
wenzelm@41497	282	"type_synonym"
wenzelm@11538	283	"typed_print_translation"
wenzelm@11538	284	"typedecl"
wenzelm@11538	285	"typedef"
wenzelm@11538	286	"ultimately"
wenzelm@11538	287	"undo"
wenzelm@11538	288	"undos_proof"
wenzelm@18541	289	"unfolding"
berghofe@26184	290	"unused_thms"
wenzelm@11538	291	"use"
wenzelm@11538	292	"use_thy"
wenzelm@12926	293	"using"
berghofe@17552	294	"value"
haftmann@31130	295	"values"
wenzelm@11538	296	"welcome"
wenzelm@11538	297	"with"
blanchet@50089	298	"wrap_data"
wenzelm@36521	299	"write"
wenzelm@11538	300	"{"
wenzelm@11538	301	"}"))
wenzelm@11538	302
wenzelm@11538	303	(defconst isar-keywords-minor
wenzelm@37785	304	'("advanced"
wenzelm@12040	305	"and"
wenzelm@12042	306	"assumes"
berghofe@16771	307	"attach"
wenzelm@24904	308	"avoids"
nipkow@15135	309	"begin"
wenzelm@11538	310	"binder"
haftmann@37824	311	"checking"
wenzelm@11538	312	"congs"
ballarin@16168	313	"constrains"
haftmann@36468	314	"datatypes"
wenzelm@50307	315	"defaults"
wenzelm@12042	316	"defines"
berghofe@17147	317	"file"
wenzelm@12042	318	"fixes"
wenzelm@19797	319	"for"
haftmann@36468	320	"functions"
wenzelm@11538	321	"hints"
haftmann@22288	322	"identifier"
wenzelm@19797	323	"if"
nipkow@15141	324	"imports"
wenzelm@11538	325	"in"
wenzelm@47946	326	"includes"
wenzelm@11661	327	"infix"
wenzelm@11538	328	"infixl"
wenzelm@11538	329	"infixr"
wenzelm@11538	330	"is"
wenzelm@47812	331	"keywords"
wenzelm@12040	332	"lazy"
haftmann@24249	333	"module_name"
wenzelm@11538	334	"monos"
wenzelm@11746	335	"morphisms"
wenzelm@50307	336	"no_dests"
wenzelm@12042	337	"notes"
wenzelm@18888	338	"obtains"
wenzelm@13364	339	"open"
wenzelm@11538	340	"output"
wenzelm@11538	341	"overloaded"
wenzelm@11618	342	"permissive"
wenzelm@33685	343	"pervasive"
wenzelm@51121	344	"rep_compat"
wenzelm@12935	345	"shows"
wenzelm@12042	346	"structure"
wenzelm@19633	347	"unchecked"
wenzelm@40632	348	"unsafe"
wenzelm@16419	349	"uses"
wenzelm@11538	350	"where"))
wenzelm@11538	351
wenzelm@11538	352	(defconst isar-keywords-control
wenzelm@25577	353	'("Isabelle\\.command"
wenzelm@25577	354	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	355	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	356	"ProofGeneral\\.kill_proof"
wenzelm@14938	357	"ProofGeneral\\.process_pgip"
wenzelm@11538	358	"ProofGeneral\\.restart"
wenzelm@11538	359	"ProofGeneral\\.undo"
wenzelm@11538	360	"cannot_undo"
wenzelm@40675	361	"cd"
wenzelm@40675	362	"commit"
wenzelm@38276	363	"disable_pr"
wenzelm@38276	364	"enable_pr"
wenzelm@11538	365	"exit"
wenzelm@11538	366	"init_toplevel"
wenzelm@11538	367	"kill"
wenzelm@38276	368	"kill_thy"
wenzelm@27538	369	"linear_undo"
wenzelm@11538	370	"quit"
wenzelm@38276	371	"remove_thy"
wenzelm@11538	372	"undo"
wenzelm@38276	373	"undos_proof"
wenzelm@38276	374	"use_thy"))
wenzelm@11538	375
wenzelm@11538	376	(defconst isar-keywords-diag
wenzelm@26482	377	'("ML_command"
wenzelm@26394	378	"ML_val"
wenzelm@33874	379	"ProofGeneral\\.pr"
wenzelm@33687	380	"boogie_status"
wenzelm@20568	381	"class_deps"
wenzelm@22864	382	"code_deps"
haftmann@22288	383	"code_thms"
wenzelm@14938	384	"display_drafts"
haftmann@24343	385	"export_code"
kleing@29819	386	"find_consts"
wenzelm@17220	387	"find_theorems"
bulwahn@47460	388	"find_unused_assms"
wenzelm@11538	389	"full_prf"
wenzelm@11538	390	"header"
wenzelm@21732	391	"help"
wenzelm@50586	392	"locale_deps"
blanchet@33198	393	"nitpick"
wenzelm@11538	394	"pr"
wenzelm@11538	395	"pretty_setmargin"
wenzelm@11538	396	"prf"
wenzelm@21732	397	"print_abbrevs"
wenzelm@11538	398	"print_antiquotations"
wenzelm@11538	399	"print_attributes"
wenzelm@11538	400	"print_binds"
blanchet@49996	401	"print_bnfs"
wenzelm@47928	402	"print_bundles"
wenzelm@11538	403	"print_cases"
wenzelm@11538	404	"print_claset"
haftmann@20378	405	"print_classes"
haftmann@31130	406	"print_codeproc"
haftmann@22288	407	"print_codesetup"
berghofe@45927	408	"print_coercion_maps"
berghofe@45927	409	"print_coercions"
wenzelm@11538	410	"print_commands"
wenzelm@24120	411	"print_configs"
wenzelm@11538	412	"print_context"
ballarin@41683	413	"print_dependencies"
wenzelm@14938	414	"print_drafts"
wenzelm@11538	415	"print_facts"
wenzelm@11661	416	"print_induct_rules"
wenzelm@51317	417	"print_inductives"
ballarin@32788	418	"print_interps"
wenzelm@12059	419	"print_locale"
wenzelm@12059	420	"print_locales"
wenzelm@11538	421	"print_methods"
ballarin@24642	422	"print_orders"
kaliszyk@35279	423	"print_quotconsts"
kaliszyk@35279	424	"print_quotients"
kuncar@48153	425	"print_quotientsQ3"
kaliszyk@35279	426	"print_quotmaps"
kuncar@48153	427	"print_quotmapsQ3"
wenzelm@12365	428	"print_rules"
wenzelm@11538	429	"print_simpset"
wenzelm@19272	430	"print_statement"
wenzelm@11538	431	"print_syntax"
wenzelm@11538	432	"print_theorems"
wenzelm@11538	433	"print_theory"
wenzelm@11538	434	"print_trans_rules"
wenzelm@11538	435	"prop"
wenzelm@11538	436	"pwd"
berghofe@14109	437	"quickcheck"
webertj@14349	438	"refute"
wenzelm@22864	439	"sledgehammer"
wenzelm@33898	440	"smt_status"
blanchet@40361	441	"solve_direct"
berghofe@41812	442	"spark_status"
wenzelm@11538	443	"term"
wenzelm@11538	444	"thm"
wenzelm@11538	445	"thm_deps"
haftmann@22486	446	"thy_deps"
blanchet@39169	447	"try"
blanchet@47512	448	"try0"
wenzelm@11538	449	"typ"
berghofe@26184	450	"unused_thms"
berghofe@17552	451	"value"
haftmann@31130	452	"values"
wenzelm@11538	453	"welcome"))
wenzelm@11538	454
wenzelm@11538	455	(defconst isar-keywords-theory-begin
wenzelm@11538	456	'("theory"))
wenzelm@11538	457
wenzelm@11538	458	(defconst isar-keywords-theory-switch
wenzelm@21302	459	'())
wenzelm@11538	460
wenzelm@11538	461	(defconst isar-keywords-theory-end
wenzelm@11538	462	'("end"))
wenzelm@11538	463
wenzelm@11538	464	(defconst isar-keywords-theory-heading
wenzelm@11538	465	'("chapter"
wenzelm@11538	466	"section"
wenzelm@11538	467	"subsection"
wenzelm@11538	468	"subsubsection"))
wenzelm@11538	469
wenzelm@11538	470	(defconst isar-keywords-theory-decl
wenzelm@26482	471	'("ML"
wenzelm@49882	472	"ML_file"
wenzelm@19069	473	"abbreviation"
wenzelm@11538	474	"arities"
wenzelm@24904	475	"atom_decl"
wenzelm@30529	476	"attribute_setup"
wenzelm@18612	477	"axiomatization"
wenzelm@11538	478	"axioms"
wenzelm@33687	479	"boogie_end"
wenzelm@33687	480	"boogie_open"
wenzelm@47928	481	"bundle"
haftmann@18552	482	"class"
wenzelm@11538	483	"classes"
wenzelm@11538	484	"classrel"
blanchet@50127	485	"codata"
haftmann@27102	486	"code_abort"
haftmann@20424	487	"code_class"
haftmann@20453	488	"code_const"
haftmann@22486	489	"code_datatype"
haftmann@24997	490	"code_include"
haftmann@20424	491	"code_instance"
wenzelm@21203	492	"code_modulename"
wenzelm@22084	493	"code_monad"
haftmann@36468	494	"code_reflect"
wenzelm@21028	495	"code_reserved"
haftmann@20453	496	"code_type"
wenzelm@11538	497	"coinductive"
berghofe@23732	498	"coinductive_set"
wenzelm@11538	499	"consts"
wenzelm@21302	500	"context"
blanchet@50127	501	"data"
wenzelm@11538	502	"datatype"
wenzelm@22084	503	"declaration"
wenzelm@23804	504	"declare"
wenzelm@36455	505	"default_sort"
wenzelm@11538	506	"defer_recdef"
wenzelm@18775	507	"definition"
wenzelm@11538	508	"defs"
wenzelm@12040	509	"domain"
wenzelm@33840	510	"domain_isomorphism"
haftmann@40822	511	"domaindef"
wenzelm@24904	512	"equivariance"
berghofe@13407	513	"extract"
berghofe@13407	514	"extract_type"
huffman@16231	515	"fixrec"
krauss@20523	516	"fun"
wenzelm@36180	517	"hide_class"
wenzelm@36180	518	"hide_const"
wenzelm@36180	519	"hide_fact"
wenzelm@36180	520	"hide_type"
wenzelm@48133	521	"import_const_map"
wenzelm@48133	522	"import_file"
wenzelm@47825	523	"import_tptp"
wenzelm@48133	524	"import_type_map"
wenzelm@11538	525	"inductive"
berghofe@23732	526	"inductive_set"
haftmann@24437	527	"instantiation"
wenzelm@11538	528	"judgment"
wenzelm@11538	529	"lemmas"
wenzelm@30463	530	"local_setup"
wenzelm@12059	531	"locale"
wenzelm@11538	532	"method_setup"
blanchet@33198	533	"nitpick_params"
wenzelm@24945	534	"no_notation"
wenzelm@15703	535	"no_syntax"
wenzelm@19255	536	"no_translations"
wenzelm@35419	537	"no_type_notation"
wenzelm@24904	538	"nominal_datatype"
wenzelm@41495	539	"nonterminal"
wenzelm@21203	540	"notation"
wenzelm@41208	541	"notepad"
wenzelm@11538	542	"oracle"
haftmann@25516	543	"overloading"
wenzelm@11538	544	"parse_ast_translation"
wenzelm@11538	545	"parse_translation"
krauss@40450	546	"partial_function"
wenzelm@11538	547	"primrec"
wenzelm@11538	548	"print_ast_translation"
wenzelm@11538	549	"print_translation"
bulwahn@46797	550	"quickcheck_generator"
berghofe@14109	551	"quickcheck_params"
berghofe@13407	552	"realizability"
berghofe@13407	553	"realizers"
wenzelm@11538	554	"recdef"
wenzelm@11538	555	"record"
webertj@14349	556	"refute_params"
wenzelm@11538	557	"setup"
kuncar@47968	558	"setup_lifting"
wenzelm@22200	559	"simproc_setup"
haftmann@36114	560	"sledgehammer_params"
berghofe@41812	561	"spark_end"
berghofe@41812	562	"spark_open"
wenzelm@49923	563	"spark_open_siv"
wenzelm@49923	564	"spark_open_vcg"
berghofe@41812	565	"spark_proof_functions"
berghofe@43227	566	"spark_types"
wenzelm@25176	567	"statespace"
wenzelm@11538	568	"syntax"
wenzelm@41034	569	"syntax_declaration"
wenzelm@11538	570	"text"
wenzelm@11538	571	"text_raw"
wenzelm@11538	572	"theorems"
wenzelm@11538	573	"translations"
wenzelm@35419	574	"type_notation"
wenzelm@41497	575	"type_synonym"
wenzelm@11538	576	"typed_print_translation"
wenzelm@11538	577	"typedecl"
wenzelm@26482	578	"use"))
wenzelm@11538	579
wenzelm@11538	580	(defconst isar-keywords-theory-script
bulwahn@37733	581	'("inductive_cases"
bulwahn@37733	582	"inductive_simps"))
wenzelm@11538	583
wenzelm@11538	584	(defconst isar-keywords-theory-goal
skalberg@14223	585	'("ax_specification"
blanchet@49996	586	"bnf_def"
wenzelm@33687	587	"boogie_vc"
bulwahn@31106	588	"code_pred"
skalberg@14223	589	"corollary"
huffman@16701	590	"cpodef"
wenzelm@41778	591	"enriched_type"
krauss@19564	592	"function"
wenzelm@11746	593	"instance"
ballarin@15598	594	"interpretation"
wenzelm@11538	595	"lemma"
huffman@48212	596	"lift_definition"
wenzelm@24904	597	"nominal_inductive"
berghofe@28656	598	"nominal_inductive2"
wenzelm@24904	599	"nominal_primrec"
huffman@16701	600	"pcpodef"
kuncar@47968	601	"quotient_definition"
kaliszyk@35279	602	"quotient_type"
wenzelm@11538	603	"recdef_tc"
haftmann@27102	604	"rep_datatype"
wenzelm@36321	605	"schematic_corollary"
wenzelm@36321	606	"schematic_lemma"
wenzelm@36321	607	"schematic_theorem"
berghofe@41812	608	"spark_vc"
skalberg@14115	609	"specification"
haftmann@24919	610	"subclass"
ballarin@28895	611	"sublocale"
krauss@19564	612	"termination"
wenzelm@11538	613	"theorem"
blanchet@50089	614	"typedef"
blanchet@50089	615	"wrap_data"))
wenzelm@11538	616
wenzelm@11538	617	(defconst isar-keywords-qed
wenzelm@11538	618	'("\\."
wenzelm@11538	619	"\\.\\."
wenzelm@11538	620	"by"
wenzelm@11538	621	"done"
wenzelm@11538	622	"sorry"))
wenzelm@11538	623
wenzelm@11538	624	(defconst isar-keywords-qed-block
wenzelm@11538	625	'("qed"))
wenzelm@11538	626
wenzelm@11538	627	(defconst isar-keywords-qed-global
wenzelm@11538	628	'("oops"))
wenzelm@11538	629
wenzelm@11538	630	(defconst isar-keywords-proof-heading
wenzelm@11538	631	'("sect"
wenzelm@11538	632	"subsect"
wenzelm@11538	633	"subsubsect"))
wenzelm@11538	634
wenzelm@11538	635	(defconst isar-keywords-proof-goal
wenzelm@29607	636	'("have"
wenzelm@11538	637	"hence"
wenzelm@29607	638	"interpret"))
wenzelm@11538	639
wenzelm@11538	640	(defconst isar-keywords-proof-block
wenzelm@11538	641	'("next"
wenzelm@11538	642	"proof"))
wenzelm@11538	643
wenzelm@11538	644	(defconst isar-keywords-proof-open
wenzelm@11538	645	'("{"))
wenzelm@11538	646
wenzelm@11538	647	(defconst isar-keywords-proof-close
wenzelm@11538	648	'("}"))
wenzelm@11538	649
wenzelm@11538	650	(defconst isar-keywords-proof-chain
wenzelm@11538	651	'("finally"
wenzelm@11538	652	"from"
wenzelm@11538	653	"then"
wenzelm@11538	654	"ultimately"
wenzelm@11538	655	"with"))
wenzelm@11538	656
wenzelm@11538	657	(defconst isar-keywords-proof-decl
wenzelm@28280	658	'("ML_prf"
wenzelm@28280	659	"also"
wenzelm@47928	660	"include"
wenzelm@47928	661	"including"
wenzelm@11538	662	"let"
wenzelm@11538	663	"moreover"
wenzelm@11538	664	"note"
wenzelm@11538	665	"txt"
wenzelm@12926	666	"txt_raw"
wenzelm@18541	667	"unfolding"
wenzelm@36521	668	"using"
wenzelm@36521	669	"write"))
wenzelm@11538	670
wenzelm@11538	671	(defconst isar-keywords-proof-asm
wenzelm@11538	672	'("assume"
wenzelm@11538	673	"case"
wenzelm@11538	674	"def"
wenzelm@11538	675	"fix"
wenzelm@11538	676	"presume"))
wenzelm@11538	677
wenzelm@11538	678	(defconst isar-keywords-proof-asm-goal
wenzelm@17850	679	'("guess"
wenzelm@21806	680	"obtain"
wenzelm@21806	681	"show"
wenzelm@21806	682	"thus"))
wenzelm@11538	683
wenzelm@11538	684	(defconst isar-keywords-proof-script
wenzelm@11538	685	'("apply"
wenzelm@11538	686	"apply_end"
wenzelm@11538	687	"back"
wenzelm@11538	688	"defer"
wenzelm@11538	689	"prefer"))
wenzelm@11538	690
wenzelm@11538	691	(provide 'isar-keywords)

author	wenzelm
	Sun, 20 Jan 2013 15:35:01 +0100
changeset 52009	9b062fef2c91
parent 51317	9149a07a6c67
child 52407	17d30843fc3b
permissions	-rw-r--r--