# HG changeset patch # User wenzelm # Date 1165953023 -3600 # Node ID 6086783d42146637db5a2eb108e6bad8564f02cb # Parent 6af1aa7f67d6e2434c7a6034daddf11aed7e82a3 updated; diff -r 6af1aa7f67d6 -r 6086783d4214 etc/isar-keywords-HOL-Nominal.el --- a/etc/isar-keywords-HOL-Nominal.el Tue Dec 12 20:49:32 2006 +0100 +++ b/etc/isar-keywords-HOL-Nominal.el Tue Dec 12 20:50:23 2006 +0100 @@ -133,6 +133,7 @@ "pretty_setmargin" "prf" "primrec" + "print_abbrevs" "print_antiquotations" "print_ast_translation" "print_attributes" @@ -312,6 +313,7 @@ "pr" "pretty_setmargin" "prf" + "print_abbrevs" "print_antiquotations" "print_attributes" "print_binds" @@ -487,9 +489,7 @@ '("have" "hence" "interpret" - "invoke" - "show" - "thus")) + "invoke")) (defconst isar-keywords-proof-block '("next" @@ -527,7 +527,9 @@ (defconst isar-keywords-proof-asm-goal '("guess" - "obtain")) + "obtain" + "show" + "thus")) (defconst isar-keywords-proof-script '("apply" diff -r 6af1aa7f67d6 -r 6086783d4214 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Dec 12 20:49:32 2006 +0100 +++ b/etc/isar-keywords-ZF.el Tue Dec 12 20:50:23 2006 +0100 @@ -452,9 +452,7 @@ '("have" "hence" "interpret" - "invoke" - "show" - "thus")) + "invoke")) (defconst isar-keywords-proof-block '("next" @@ -492,7 +490,9 @@ (defconst isar-keywords-proof-asm-goal '("guess" - "obtain")) + "obtain" + "show" + "thus")) (defconst isar-keywords-proof-script '("apply" diff -r 6af1aa7f67d6 -r 6086783d4214 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Dec 12 20:49:32 2006 +0100 +++ b/etc/isar-keywords.el Tue Dec 12 20:50:23 2006 +0100 @@ -510,9 +510,7 @@ '("have" "hence" "interpret" - "invoke" - "show" - "thus")) + "invoke")) (defconst isar-keywords-proof-block '("next" @@ -550,7 +548,9 @@ (defconst isar-keywords-proof-asm-goal '("guess" - "obtain")) + "obtain" + "show" + "thus")) (defconst isar-keywords-proof-script '("apply"