# HG changeset patch
# User berghofe
# Date 1027259559 -7200
# Node ID d128b5915f6b524a04e0e255e61b354e9c6980fc
# Parent  d587db56ee027f4b9aead7e358e02cbf681e7f76
Added program extraction keywords.

diff -r d587db56ee02 -r d128b5915f6b etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sun Jul 21 15:45:41 2002 +0200
+++ b/etc/isar-keywords-ZF.el	Sun Jul 21 15:52:39 2002 +0200
@@ -53,6 +53,8 @@
     "enable_pr"
     "end"
     "exit"
+    "extract"
+    "extract_type"
     "finally"
     "fix"
     "from"
@@ -117,6 +119,8 @@
     "pwd"
     "qed"
     "quit"
+    "realizability"
+    "realizers"
     "redo"
     "remove_thy"
     "rep_datatype"
@@ -297,6 +301,8 @@
     "datatype"
     "defaultsort"
     "defs"
+    "extract"
+    "extract_type"
     "generate_code"
     "global"
     "hide"
@@ -313,6 +319,8 @@
     "primrec"
     "print_ast_translation"
     "print_translation"
+    "realizability"
+    "realizers"
     "rep_datatype"
     "setup"
     "syntax"
diff -r d587db56ee02 -r d128b5915f6b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sun Jul 21 15:45:41 2002 +0200
+++ b/etc/isar-keywords.el	Sun Jul 21 15:52:39 2002 +0200
@@ -55,6 +55,8 @@
     "enable_pr"
     "end"
     "exit"
+    "extract"
+    "extract_type"
     "finally"
     "fix"
     "from"
@@ -118,6 +120,8 @@
     "pwd"
     "qed"
     "quit"
+    "realizability"
+    "realizers"
     "recdef"
     "recdef_tc"
     "record"
@@ -319,6 +323,8 @@
     "defer_recdef"
     "defs"
     "domain"
+    "extract"
+    "extract_type"
     "generate_code"
     "global"
     "hide"
@@ -335,6 +341,8 @@
     "primrec"
     "print_ast_translation"
     "print_translation"
+    "realizability"
+    "realizers"
     "recdef"
     "record"
     "rep_datatype"