import -> imports
authornipkow
Wed Aug 18 11:44:17 2004 +0200 (2004-08-18)
changeset 15141a95c2ff210ba
parent 15140 322485b816ac
child 15142 7b7109f22224
import -> imports
doc-src/TutorialI/Documents/Documents.thy
doc-src/TutorialI/Documents/document/Documents.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/ToyList2/ToyList1
doc-src/TutorialI/basics.tex
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/thy_header.ML
     1.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:09:40 2004 +0200
     1.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Aug 18 11:44:17 2004 +0200
     1.3 @@ -490,7 +490,7 @@
     1.4    header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
     1.5  
     1.6    theory Foo_Bar
     1.7 -  import Main
     1.8 +  imports Main
     1.9    begin
    1.10  
    1.11    subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
    1.12 @@ -767,7 +767,7 @@
    1.13    \begin{tabular}{l}
    1.14    \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
    1.15    \texttt{theory T} \\
    1.16 -  \texttt{import Main} \\
    1.17 +  \texttt{imports Main} \\
    1.18    \texttt{begin} \\
    1.19    \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
    1.20    ~~$\vdots$ \\
     2.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:09:40 2004 +0200
     2.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Aug 18 11:44:17 2004 +0200
     2.3 @@ -504,7 +504,7 @@
     2.4    header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
     2.5  
     2.6    theory Foo_Bar
     2.7 -  import Main
     2.8 +  imports Main
     2.9    begin
    2.10  
    2.11    subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
    2.12 @@ -796,7 +796,7 @@
    2.13    \begin{tabular}{l}
    2.14    \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
    2.15    \texttt{theory T} \\
    2.16 -  \texttt{import Main} \\
    2.17 +  \texttt{imports Main} \\
    2.18    \texttt{begin} \\
    2.19    \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
    2.20    ~~$\vdots$ \\
     3.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 18 11:09:40 2004 +0200
     3.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 18 11:44:17 2004 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4  theory ToyList
     3.5 -import PreList
     3.6 +imports PreList
     3.7  begin
     3.8  
     3.9  text{*\noindent
     4.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:09:40 2004 +0200
     4.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed Aug 18 11:44:17 2004 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4  \begin{isabellebody}%
     4.5  \def\isabellecontext{ToyList}%
     4.6  \isacommand{theory}\ ToyList\isanewline
     4.7 -\isakeyword{import}\ PreList\isanewline
     4.8 +\isakeyword{imports}\ PreList\isanewline
     4.9  \isakeyword{begin}\isamarkupfalse%
    4.10  %
    4.11  \begin{isamarkuptext}%
     5.1 --- a/doc-src/TutorialI/ToyList2/ToyList1	Wed Aug 18 11:09:40 2004 +0200
     5.2 +++ b/doc-src/TutorialI/ToyList2/ToyList1	Wed Aug 18 11:44:17 2004 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4  theory ToyList
     5.5 -import PreList
     5.6 +imports PreList
     5.7  begin
     5.8  
     5.9  datatype 'a list = Nil                          ("[]")
     6.1 --- a/doc-src/TutorialI/basics.tex	Wed Aug 18 11:09:40 2004 +0200
     6.2 +++ b/doc-src/TutorialI/basics.tex	Wed Aug 18 11:44:17 2004 +0200
     6.3 @@ -53,7 +53,7 @@
     6.4  format of a theory \texttt{T} is
     6.5  \begin{ttbox}
     6.6  theory T
     6.7 -import B\(@1\) \(\ldots\) B\(@n\)
     6.8 +imports B\(@1\) \(\ldots\) B\(@n\)
     6.9  begin
    6.10  {\rmfamily\textit{declarations, definitions, and proofs}}
    6.11  end
     7.1 --- a/etc/isar-keywords-ZF.el	Wed Aug 18 11:09:40 2004 +0200
     7.2 +++ b/etc/isar-keywords-ZF.el	Wed Aug 18 11:44:17 2004 +0200
     7.3 @@ -193,7 +193,7 @@
     7.4      "elimination"
     7.5      "files"
     7.6      "fixes"
     7.7 -    "import"
     7.8 +    "imports"
     7.9      "in"
    7.10      "includes"
    7.11      "induction"
     8.1 --- a/etc/isar-keywords.el	Wed Aug 18 11:09:40 2004 +0200
     8.2 +++ b/etc/isar-keywords.el	Wed Aug 18 11:44:17 2004 +0200
     8.3 @@ -204,7 +204,7 @@
     8.4      "fixes"
     8.5      "hide_action"
     8.6      "hints"
     8.7 -    "import"
     8.8 +    "imports"
     8.9      "in"
    8.10      "includes"
    8.11      "induction"
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 18 11:09:40 2004 +0200
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 18 11:44:17 2004 +0200
     9.3 @@ -755,7 +755,7 @@
     9.4  val keywords =
     9.5   ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
     9.6    "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "begin",
     9.7 -  "binder", "concl", "defines", "files", "fixes", "import", "in", "includes",
     9.8 +  "binder", "concl", "defines", "files", "fixes", "imports", "in", "includes",
     9.9    "infix", "infixl", "infixr", "is", "notes", "open", "output",
    9.10    "overloaded", "shows", "structure", "where", "|", "\\<equiv>",
    9.11    "\\<leftharpoondown>", "\\<rightharpoonup>",
    10.1 --- a/src/Pure/Isar/thy_header.ML	Wed Aug 18 11:09:40 2004 +0200
    10.2 +++ b/src/Pure/Isar/thy_header.ML	Wed Aug 18 11:44:17 2004 +0200
    10.3 @@ -40,9 +40,11 @@
    10.4  
    10.5  val headerN = "header";
    10.6  val theoryN = "theory";
    10.7 +val importsN = "imports";
    10.8  
    10.9  val theory_keyword = P.$$$ theoryN;
   10.10  val header_keyword = P.$$$ headerN;
   10.11 +val imports_keyword = P.$$$ importsN;
   10.12  
   10.13  
   10.14  (* detect new/old headers *)
   10.15 @@ -57,14 +59,14 @@
   10.16  (* scan old/new headers *)
   10.17  
   10.18  val header_lexicon = T.make_lexicon
   10.19 -  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, "import", theoryN];
   10.20 +  ["(", ")", "+", ":", ";", "=", "begin", "files", headerN, importsN, theoryN];
   10.21  
   10.22  val file_name =
   10.23    (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
   10.24  
   10.25  val args =
   10.26    (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name ||
   10.27 -              P.$$$ "import" |-- Scan.repeat1 P.name) --
   10.28 +              imports_keyword |-- Scan.repeat1 P.name) --
   10.29      Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|
   10.30    (P.$$$ ":" || P.$$$ "begin"))
   10.31    >> (fn ((A, Bs), files) => (A, Bs, files));