# HG changeset patch
# User nipkow
# Date 1092822257 -7200
# Node ID a95c2ff210ba5302ca50983369943719134da271
# Parent  322485b816ac88054c4505e1ebee0c72152e09d6
import -> imports

diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:44:17 2004 +0200
@@ -490,7 +490,7 @@
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
-  import Main
+  imports Main
   begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
@@ -767,7 +767,7 @@
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
   \texttt{theory T} \\
-  \texttt{import Main} \\
+  \texttt{imports Main} \\
   \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:44:17 2004 +0200
@@ -504,7 +504,7 @@
   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
 
   theory Foo_Bar
-  import Main
+  imports Main
   begin
 
   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
@@ -796,7 +796,7 @@
   \begin{tabular}{l}
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
   \texttt{theory T} \\
-  \texttt{import Main} \\
+  \texttt{imports Main} \\
   \texttt{begin} \\
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
   ~~$\vdots$ \\
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 18 11:44:17 2004 +0200
@@ -1,5 +1,5 @@
 theory ToyList
-import PreList
+imports PreList
 begin
 
 text{*\noindent
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:44:17 2004 +0200
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{ToyList}%
 \isacommand{theory}\ ToyList\isanewline
-\isakeyword{import}\ PreList\isanewline
+\isakeyword{imports}\ PreList\isanewline
 \isakeyword{begin}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/ToyList2/ToyList1
--- a/doc-src/TutorialI/ToyList2/ToyList1	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/ToyList2/ToyList1	Wed Aug 18 11:44:17 2004 +0200
@@ -1,5 +1,5 @@
 theory ToyList
-import PreList
+imports PreList
 begin
 
 datatype 'a list = Nil                          ("[]")
diff -r 322485b816ac -r a95c2ff210ba doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Aug 18 11:09:40 2004 +0200
+++ b/doc-src/TutorialI/basics.tex	Wed Aug 18 11:44:17 2004 +0200
@@ -53,7 +53,7 @@
 format of a theory \texttt{T} is
 \begin{ttbox}
 theory T
-import B\(@1\) \(\ldots\) B\(@n\)
+imports B\(@1\) \(\ldots\) B\(@n\)
 begin
 {\rmfamily\textit{declarations, definitions, and proofs}}
 end
diff -r 322485b816ac -r a95c2ff210ba etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Aug 18 11:09:40 2004 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Aug 18 11:44:17 2004 +0200
@@ -193,7 +193,7 @@
     "elimination"
     "files"
     "fixes"
-    "import"
+    "imports"
     "in"
     "includes"
     "induction"
diff -r 322485b816ac -r a95c2ff210ba etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Aug 18 11:09:40 2004 +0200
+++ b/etc/isar-keywords.el	Wed Aug 18 11:44:17 2004 +0200
@@ -204,7 +204,7 @@
     "fixes"
     "hide_action"
     "hints"
-    "import"
+    "imports"
     "in"
     "includes"
     "induction"
diff -r 322485b816ac -r a95c2ff210ba src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 18 11:09:40 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 18 11:44:17 2004 +0200
@@ -755,7 +755,7 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
-  "binder", "concl", "defines", "files", "fixes", "import", "in", "includes",
+  "binder", "concl", "defines", "files", "fixes", "imports", "in", "includes",
   "infix", "infixl", "infixr", "is", "notes", "open", "output",
   "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",
diff -r 322485b816ac -r a95c2ff210ba src/Pure/Isar/thy_header.ML
--- a/src/Pure/Isar/thy_header.ML	Wed Aug 18 11:09:40 2004 +0200
+++ b/src/Pure/Isar/thy_header.ML	Wed Aug 18 11:44:17 2004 +0200
@@ -40,9 +40,11 @@
 
 val headerN = "header";
 val theoryN = "theory";
+val importsN = "imports";
 
 val theory_keyword = P.$$$ theoryN;
 val header_keyword = P.$$$ headerN;
+val imports_keyword = P.$$$ importsN;
 
 
 (* detect new/old headers *)
@@ -57,14 +59,14 @@
 (* scan old/new headers *)
 
 val header_lexicon = T.make_lexicon
-  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, "import", theoryN];
+  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, importsN, theoryN];
 
 val file_name =
   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
 
 val args =
   (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name ||
-              P.$$$ "import" |-- Scan.repeat1 P.name) --
+              imports_keyword |-- Scan.repeat1 P.name) --
     Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|
   (P.$$$ ":" || P.$$$ "begin"))
   >> (fn ((A, Bs), files) => (A, Bs, files));