1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Tue Dec 12 20:49:32 2006 +0100
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Tue Dec 12 20:50:23 2006 +0100
     1.3 @@ -133,6 +133,7 @@
     1.4      "pretty_setmargin"
     1.5      "prf"
     1.6      "primrec"
     1.7 +    "print_abbrevs"
     1.8      "print_antiquotations"
     1.9      "print_ast_translation"
    1.10      "print_attributes"
    1.11 @@ -312,6 +313,7 @@
    1.12      "pr"
    1.13      "pretty_setmargin"
    1.14      "prf"
    1.15 +    "print_abbrevs"
    1.16      "print_antiquotations"
    1.17      "print_attributes"
    1.18      "print_binds"
    1.19 @@ -487,9 +489,7 @@
    1.20    '("have"
    1.21      "hence"
    1.22      "interpret"
    1.23 -    "invoke"
    1.24 -    "show"
    1.25 -    "thus"))
    1.26 +    "invoke"))
    1.27  
    1.28  (defconst isar-keywords-proof-block
    1.29    '("next"
    1.30 @@ -527,7 +527,9 @@
    1.31  
    1.32  (defconst isar-keywords-proof-asm-goal
    1.33    '("guess"
    1.34 -    "obtain"))
    1.35 +    "obtain"
    1.36 +    "show"
    1.37 +    "thus"))
    1.38  
    1.39  (defconst isar-keywords-proof-script
    1.40    '("apply"

     2.1 --- a/etc/isar-keywords-ZF.el	Tue Dec 12 20:49:32 2006 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Dec 12 20:50:23 2006 +0100
     2.3 @@ -452,9 +452,7 @@
     2.4    '("have"
     2.5      "hence"
     2.6      "interpret"
     2.7 -    "invoke"
     2.8 -    "show"
     2.9 -    "thus"))
    2.10 +    "invoke"))
    2.11  
    2.12  (defconst isar-keywords-proof-block
    2.13    '("next"
    2.14 @@ -492,7 +490,9 @@
    2.15  
    2.16  (defconst isar-keywords-proof-asm-goal
    2.17    '("guess"
    2.18 -    "obtain"))
    2.19 +    "obtain"
    2.20 +    "show"
    2.21 +    "thus"))
    2.22  
    2.23  (defconst isar-keywords-proof-script
    2.24    '("apply"

     3.1 --- a/etc/isar-keywords.el	Tue Dec 12 20:49:32 2006 +0100
     3.2 +++ b/etc/isar-keywords.el	Tue Dec 12 20:50:23 2006 +0100
     3.3 @@ -510,9 +510,7 @@
     3.4    '("have"
     3.5      "hence"
     3.6      "interpret"
     3.7 -    "invoke"
     3.8 -    "show"
     3.9 -    "thus"))
    3.10 +    "invoke"))
    3.11  
    3.12  (defconst isar-keywords-proof-block
    3.13    '("next"
    3.14 @@ -550,7 +548,9 @@
    3.15  
    3.16  (defconst isar-keywords-proof-asm-goal
    3.17    '("guess"
    3.18 -    "obtain"))
    3.19 +    "obtain"
    3.20 +    "show"
    3.21 +    "thus"))
    3.22  
    3.23  (defconst isar-keywords-proof-script
    3.24    '("apply"