nominal2: isar-keywords-prove.el@6348c2a57ec2 (annotated)

6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	;;
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	;; Keyword classification tables for Isabelle/Isar.
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	3	;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test + HOL-Nominal.
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	;;
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	(defconst isar-keywords-major
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	'("\\."
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	"\\.\\."
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	"Isabelle\\.command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	"Isar\\.begin_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"Isar\\.define_command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	"Isar\\.edit_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	"Isar\\.end_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	"ML"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	"ML_command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	"ML_prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	"ML_val"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	"ProofGeneral\\.inform_file_processed"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	"ProofGeneral\\.inform_file_retracted"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	"ProofGeneral\\.kill_proof"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	"ProofGeneral\\.process_pgip"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	"ProofGeneral\\.restart"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	"ProofGeneral\\.undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	"abbreviation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	"also"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	"apply"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	"apply_end"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	"arities"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	"assume"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	31	"atom_decl"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	"atp_info"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	"atp_kill"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	"atp_messages"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	"atp_minimize"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	"attribute_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	"ax_specification"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	"axclass"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	"axiomatization"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	"axioms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	"back"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	"by"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	"cannot_undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	"case"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	"cd"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	"chapter"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	"class"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	"class_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	"classes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	"classrel"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	"code_abort"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	"code_class"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	"code_const"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	"code_datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	"code_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	"code_include"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	"code_instance"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	"code_library"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	"code_module"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	"code_modulename"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	"code_monad"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	"code_pred"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	"code_reserved"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	"code_thms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	"code_type"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	"coinductive"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	"coinductive_set"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	"commit"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	"constdefs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	"consts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	"consts_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	"context"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	"corollary"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	"datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	"declaration"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	"declare"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	"def"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	"defaultsort"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	"defer"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	"defer_recdef"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	"definition"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	"defs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	"disable_pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	"display_drafts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	"done"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	"enable_pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	"end"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	88	"equivariance"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	"exit"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	"export_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	"extract"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	"extract_type"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	"finalconsts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	"finally"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	"find_consts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	96	"find_theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	"fix"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	"from"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	"full_prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	"fun"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	"function"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	"global"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	"guess"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	"have"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	"header"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	"help"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	"hence"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	"hide"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	"inductive"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	"inductive_cases"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	"inductive_set"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	"init_toplevel"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	"instance"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	"instantiation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	"interpret"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	"interpretation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	"judgment"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	"kill"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	"kill_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	"lemma"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	"lemmas"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	"let"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	"linear_undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	"local"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	"local_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	"locale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	"method_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	"moreover"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	"next"
221 f219011a5e3c Fixes Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 200 diff changeset	130	"nitpick"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	"no_notation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	"no_syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	133	"no_translations"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	134	"nominal_datatype"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	135	"nominal_inductive"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	136	"nominal_inductive2"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	137	"nominal_primrec"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	"nonterminals"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	"normal_form"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	"notation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	"note"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	"obtain"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	"oops"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	"oracle"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	"overloading"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	"parse_ast_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	147	"parse_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	"pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	"prefer"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	"presume"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	"pretty_setmargin"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	"prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	"primrec"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	"print_abbrevs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	"print_antiquotations"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	"print_ast_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	"print_atps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	"print_attributes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	"print_binds"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	"print_cases"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	"print_claset"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	162	"print_classes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	163	"print_codeproc"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	164	"print_codesetup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	165	"print_commands"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	166	"print_configs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	167	"print_context"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	168	"print_drafts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	169	"print_facts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	170	"print_induct_rules"
184 f3c192574d2a added "print_quotients" command to th ekeyword file Christian Urban <urbanc@in.tum.de> parents: 78 diff changeset	171	"print_interps"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	172	"print_locale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	"print_locales"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	174	"print_methods"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	"print_orders"
184 f3c192574d2a added "print_quotients" command to th ekeyword file Christian Urban <urbanc@in.tum.de> parents: 78 diff changeset	176	"print_quotients"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	"print_rules"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	178	"print_simpset"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	"print_statement"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	"print_syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	"print_theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	182	"print_theory"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	"print_trans_rules"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	184	"print_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	"proof"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	186	"prop"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	187	"prove"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	188	"pwd"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	189	"qed"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	190	"quickcheck"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	"quickcheck_params"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	"quit"
78 2374d50fc6dd added new keyword Christian Urban <urbanc@in.tum.de> parents: 6 diff changeset	193	"quotient"
186 9ca545f783f6 updated with quotient_def Christian Urban <urbanc@in.tum.de> parents: 184 diff changeset	194	"quotient_def"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	"realizability"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	196	"realizers"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	197	"recdef"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	198	"recdef_tc"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	199	"record"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	"refute"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	201	"refute_params"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	202	"remove_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	"rep_datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	204	"sect"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	"section"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	"setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	207	"show"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	208	"simproc_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	209	"sledgehammer"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	"sorry"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	211	"specification"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	212	"subclass"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	"sublocale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	214	"subsect"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	215	"subsection"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	216	"subsubsect"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	"subsubsection"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	"syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	"term"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	220	"termination"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	221	"text"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	"text_raw"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	"then"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	224	"theorem"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	225	"theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	"theory"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	"thm"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	228	"thm_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	229	"thus"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	230	"thy_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	231	"touch_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	232	"translations"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	233	"txt"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	234	"txt_raw"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	235	"typ"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	236	"typed_print_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	237	"typedecl"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	238	"typedef"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	"types"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	240	"types_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	"ultimately"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	242	"undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	243	"undos_proof"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	244	"unfolding"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	245	"unused_thms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	246	"use"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	247	"use_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	248	"using"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	249	"value"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	250	"values"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	251	"welcome"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	252	"with"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	253	"{"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	254	"}"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	255
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	256	(defconst isar-keywords-minor
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	257	'("advanced"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	258	"and"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	259	"assumes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	260	"attach"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	261	"avoids"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	"begin"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	"binder"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	264	"congs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	265	"constrains"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	"contains"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	267	"defines"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	268	"file"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	"fixes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	270	"for"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	"hints"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	"identifier"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	273	"if"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	"imports"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	275	"in"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	276	"infix"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	277	"infixl"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	278	"infixr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	279	"is"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	280	"module_name"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	281	"monos"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	282	"morphisms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	283	"notes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	284	"obtains"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	285	"open"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	286	"output"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	287	"overloaded"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	288	"permissive"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	289	"shows"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	290	"structure"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	291	"unchecked"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	292	"uses"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	293	"where"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	294
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	295	(defconst isar-keywords-control
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	296	'("Isabelle\\.command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	297	"Isar\\.begin_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	298	"Isar\\.define_command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	299	"Isar\\.edit_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	300	"Isar\\.end_document"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	301	"ProofGeneral\\.inform_file_processed"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	302	"ProofGeneral\\.inform_file_retracted"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	303	"ProofGeneral\\.kill_proof"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	304	"ProofGeneral\\.process_pgip"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	305	"ProofGeneral\\.restart"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	306	"ProofGeneral\\.undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	307	"cannot_undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	308	"exit"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	309	"init_toplevel"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	310	"kill"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	311	"linear_undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	312	"quit"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	313	"undo"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	314	"undos_proof"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	315
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	316	(defconst isar-keywords-diag
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	317	'("ML_command"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	"ML_val"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	319	"atp_info"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	320	"atp_kill"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	321	"atp_messages"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	322	"atp_minimize"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	323	"cd"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	"class_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	325	"code_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	326	"code_thms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	327	"commit"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	328	"disable_pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	329	"display_drafts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	330	"enable_pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	331	"export_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	332	"find_consts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	333	"find_theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	334	"full_prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	335	"header"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	336	"help"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	337	"kill_thy"
233 fcff14e578d3 Fixed wrong CARD definition and removed the "Does not work anymore" comment. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 221 diff changeset	338	"nitpick"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	339	"normal_form"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	340	"pr"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	341	"pretty_setmargin"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	342	"prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	343	"print_abbrevs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	344	"print_antiquotations"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	345	"print_atps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	346	"print_attributes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	"print_binds"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	348	"print_cases"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	349	"print_claset"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	350	"print_classes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	351	"print_codeproc"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	352	"print_codesetup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	353	"print_commands"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	354	"print_configs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	355	"print_context"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	356	"print_drafts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	357	"print_facts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	358	"print_induct_rules"
184 f3c192574d2a added "print_quotients" command to th ekeyword file Christian Urban <urbanc@in.tum.de> parents: 78 diff changeset	359	"print_interps"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	360	"print_locale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	361	"print_locales"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	362	"print_methods"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	363	"print_orders"
184 f3c192574d2a added "print_quotients" command to th ekeyword file Christian Urban <urbanc@in.tum.de> parents: 78 diff changeset	364	"print_quotients"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	365	"print_rules"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	"print_simpset"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	367	"print_statement"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	368	"print_syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	369	"print_theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	370	"print_theory"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	371	"print_trans_rules"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	372	"prop"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	373	"pwd"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	374	"quickcheck"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	375	"refute"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	376	"remove_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	377	"sledgehammer"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	378	"term"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	379	"thm"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	380	"thm_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	381	"thy_deps"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	382	"touch_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	383	"typ"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	384	"unused_thms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	385	"use_thy"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	386	"value"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	387	"values"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	388	"welcome"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	389
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	390	(defconst isar-keywords-theory-begin
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	'("theory"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	392
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	393	(defconst isar-keywords-theory-switch
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	394	'())
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	395
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	396	(defconst isar-keywords-theory-end
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	397	'("end"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	398
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	399	(defconst isar-keywords-theory-heading
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	400	'("chapter"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	401	"section"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	402	"subsection"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	403	"subsubsection"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	404
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	405	(defconst isar-keywords-theory-decl
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	406	'("ML"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	407	"abbreviation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	408	"arities"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	409	"atom_decl"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	410	"attribute_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	411	"axclass"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	412	"axiomatization"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	413	"axioms"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	414	"class"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	415	"classes"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	416	"classrel"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	417	"code_abort"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	418	"code_class"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	419	"code_const"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	"code_datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	421	"code_include"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	422	"code_instance"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	423	"code_library"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	424	"code_module"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	425	"code_modulename"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	426	"code_monad"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	427	"code_reserved"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	428	"code_type"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	429	"coinductive"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	430	"coinductive_set"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	431	"constdefs"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	432	"consts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	433	"consts_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	434	"context"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	435	"datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	436	"declaration"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	437	"declare"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	438	"defaultsort"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	439	"defer_recdef"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	440	"definition"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	441	"defs"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	442	"equivariance"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	443	"extract"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	444	"extract_type"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	445	"finalconsts"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	446	"fun"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	447	"global"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	448	"hide"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	449	"inductive"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	450	"inductive_set"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	451	"instantiation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	452	"judgment"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	453	"lemmas"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	454	"local"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	455	"local_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	456	"locale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	457	"method_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	458	"no_notation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	459	"no_syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	460	"no_translations"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	461	"nominal_datatype"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	462	"nonterminals"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	463	"notation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	464	"oracle"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	465	"overloading"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	466	"parse_ast_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	467	"parse_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	468	"primrec"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	469	"print_ast_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	470	"print_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	471	"quickcheck_params"
186 9ca545f783f6 updated with quotient_def Christian Urban <urbanc@in.tum.de> parents: 184 diff changeset	472	"quotient_def"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	473	"realizability"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	474	"realizers"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	475	"recdef"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	476	"record"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	477	"refute_params"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	478	"setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	479	"simproc_setup"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	480	"syntax"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	481	"text"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	482	"text_raw"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	483	"theorems"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	484	"translations"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	485	"typed_print_translation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	486	"typedecl"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	487	"types"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	488	"types_code"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	489	"use"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	490
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	491	(defconst isar-keywords-theory-script
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	492	'("inductive_cases"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	493
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	494	(defconst isar-keywords-theory-goal
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	495	'("ax_specification"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	496	"code_pred"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	497	"corollary"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	498	"function"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	499	"instance"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	500	"interpretation"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	501	"lemma"
200 d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	502	"nominal_inductive"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	503	"nominal_inductive2"
d6a24dad5882 made quotients compatiple with Nominal; updated keyword file Christian Urban <urbanc@in.tum.de> parents: 186 diff changeset	504	"nominal_primrec"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	505	"prove"
78 2374d50fc6dd added new keyword Christian Urban <urbanc@in.tum.de> parents: 6 diff changeset	506	"quotient"
6 6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	507	"recdef_tc"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	508	"rep_datatype"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	509	"specification"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	510	"subclass"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	511	"sublocale"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	512	"termination"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	513	"theorem"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	514	"typedef"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	515
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	516	(defconst isar-keywords-qed
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	517	'("\\."
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	518	"\\.\\."
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	519	"by"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	520	"done"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	521	"sorry"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	522
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	523	(defconst isar-keywords-qed-block
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	524	'("qed"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	525
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	526	(defconst isar-keywords-qed-global
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	527	'("oops"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	528
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	529	(defconst isar-keywords-proof-heading
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	530	'("sect"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	531	"subsect"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	532	"subsubsect"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	533
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	534	(defconst isar-keywords-proof-goal
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	535	'("have"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	536	"hence"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	537	"interpret"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	538
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	539	(defconst isar-keywords-proof-block
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	540	'("next"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	541	"proof"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	542
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	543	(defconst isar-keywords-proof-open
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	544	'("{"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	545
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	546	(defconst isar-keywords-proof-close
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	547	'("}"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	548
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	549	(defconst isar-keywords-proof-chain
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	550	'("finally"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	551	"from"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	552	"then"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	553	"ultimately"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	554	"with"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	555
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	556	(defconst isar-keywords-proof-decl
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	557	'("ML_prf"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	558	"also"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	559	"let"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	560	"moreover"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	561	"note"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	562	"txt"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	563	"txt_raw"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	564	"unfolding"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	565	"using"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	566
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	567	(defconst isar-keywords-proof-asm
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	568	'("assume"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	569	"case"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	570	"def"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	571	"fix"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	572	"presume"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	573
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	574	(defconst isar-keywords-proof-asm-goal
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	575	'("guess"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	576	"obtain"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	577	"show"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	578	"thus"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	579
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	580	(defconst isar-keywords-proof-script
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	581	'("apply"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	582	"apply_end"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	583	"back"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	584	"defer"
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	585	"prefer"))
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	586
6a1b4c22a386 added the prove command Christian Urban <urbanc@in.tum.de> parents: diff changeset	587	(provide 'isar-keywords)

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Fri, 04 Dec 2009 15:18:33 +0100
changeset 529	6348c2a57ec2
parent 233	fcff14e578d3
child 663	0dd10a900cae
permissions	-rw-r--r--