# HG changeset patch # User clasohm # Date 753011759 -3600 # Node ID 0872fd327440dd188c1868d77cded6b84ae0c4a4 # Parent e332c5bf9e1fe2a98abb295185cc4867139b37bb adapted "Defining theories" to new use_thy diff -r e332c5bf9e1f -r 0872fd327440 doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Thu Nov 11 10:43:37 1993 +0100 +++ b/doc-src/Intro/advanced.tex Thu Nov 11 10:55:59 1993 +0100 @@ -377,16 +377,16 @@ a given theory; \ttindexbold{use_thy} automatically loads a theory's parents before loading the theory itself. -Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads a theory from -the file {\it tf}{\tt.thy}, writes the corresponding {\ML} code to the file -{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. This declares the -{\ML} structure~$T$, which contains a component {\tt thy} denoting the new -theory, a component for each rule, and everything declared in {\it ML - code}. +Calling \ttindexbold{use_thy}~{\tt"}{\it T\/}{\tt"} reads a theory from the +file {\it t}{\tt.thy}, writes the corresponding {\ML} code to the file +{\tt.}{\it t}{\tt.thy.ML}, reads the latter file, and deletes it if no errors +occured. This declares the {\ML} structure~$T$, which contains a component +{\tt thy} denoting the new theory, a component for each rule, and everything +declared in {\it ML code}. Errors may arise during the translation to {\ML} (say, a misspelled keyword) or during creation of the new theory (say, a type error in a rule). But if -all goes well, {\tt use_thy} will finally read the file {\it tf}{\tt.ML}, if +all goes well, {\tt use_thy} will finally read the file {\it t}{\tt.ML}, if it exists. This file typically begins with the {\ML} declaration {\tt open}~$T$ and contains proofs that refer to the components of~$T$. Theories can be defined directly by issuing {\ML} declarations to Isabelle,