# HG changeset patch # User Christian Urban # Date 1255380256 -7200 # Node ID 2374d50fc6dd20f7c9bae8f188b56eaa53135b29 # Parent cb74afa437d72fe108dac741b84a0e674d2f481b added new keyword diff -r cb74afa437d7 -r 2374d50fc6dd isar-keywords-prove.el --- a/isar-keywords-prove.el Mon Oct 12 16:31:29 2009 +0200 +++ b/isar-keywords-prove.el Mon Oct 12 22:44:16 2009 +0200 @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Command. +;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Nominal-Prove. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; @@ -9,12 +9,9 @@ "\\.\\." "Isabelle\\.command" "Isar\\.begin_document" - "Isar\\.command" "Isar\\.define_command" "Isar\\.edit_document" "Isar\\.end_document" - "Isar\\.insert" - "Isar\\.remove" "ML" "ML_command" "ML_prf" @@ -184,6 +181,7 @@ "quickcheck" "quickcheck_params" "quit" + "quotient" "realizability" "realizers" "recdef" @@ -286,12 +284,9 @@ (defconst isar-keywords-control '("Isabelle\\.command" "Isar\\.begin_document" - "Isar\\.command" "Isar\\.define_command" "Isar\\.edit_document" "Isar\\.end_document" - "Isar\\.insert" - "Isar\\.remove" "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" "ProofGeneral\\.kill_proof" @@ -487,6 +482,7 @@ "interpretation" "lemma" "prove" + "quotient" "recdef_tc" "rep_datatype" "specification"