Old stuff.
--- a/doc-src/Pure/theory-extensions Tue Apr 27 10:52:25 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-The new Internal Interface for Theory Extension
-===============================================
-
-MMW 06-Jun-1994
-
-
-In former versions of Isabelle, the interface for theory extension was
-provided by extend_theory. This had many deficiencies and has been removed in
-Isabelle94/2.
-
-Instead of one monolithic function, there is now a host of small functions of
-the form:
-
- add_XXX: ... -> theory -> theory
-
-These provide an extension mechanism which is:
-
- - incremental (but non-destructive):
-
- An extend operation may now involve many functions of the add_XXX kind.
- These act in a purely functional manner.
-
- - nameless:
-
- One no longer needs to invent new theory names for intermediate theories.
- There's now a notion of _draft_theories_ that behave like ordinary ones
- in many cases (main exceptions: extensions of drafts are not related (wrt
- subthy); merges of drafts with unrelated theories are impossible). A
- draft is "closed" by add_thyname.
-
- - extendable:
-
- Package writers simply have to provide add_XXX like functions, which are
- built using a basic set provided by Pure Isabelle.
-
-
-Here follows a sample interactive session using the new functions:
-
- > add_consts
- # [("nand", "[o, o] => o", NoSyn), ("#", "[o, o] => o", Infixl 30)]
- # FOL.thy;
- Building new grammar...
- val it = {Pure, IFOL, FOL, #} : theory
- > add_axioms
- # [("nand_def", "nand(P, Q) == ~(P & Q)"), ("xor_def", "P # Q == P & ~Q | ~P & Q")]
- # it;
- val it = {Pure, IFOL, FOL, #} : theory
- > add_thyname "Gate" it;
- val it = {Pure, IFOL, FOL, Gate} : theory
-
-Note that theories and theorems with a "#" draft stamp are not supposed to
-persist. Typically, there is a final add_thyname somewhere with the "real"
-theory name as supplied by the user.
-
-
-Appendix A: Basic theory extension functions
---------------------------------------------
-
- val add_classes: (class list * class * class list) list -> theory -> theory
- val add_defsort: sort -> theory -> theory
- val add_types: (string * int * mixfix) list -> theory -> theory
- val add_tyabbrs: (string * string list * string * mixfix) list
- -> theory -> theory
- val add_tyabbrs_i: (string * string list * typ * mixfix) list
- -> theory -> theory
- val add_arities: (string * sort list * sort) list -> theory -> theory
- val add_consts: (string * string * mixfix) list -> theory -> theory
- val add_consts_i: (string * typ * mixfix) list -> theory -> theory
- val add_syntax: (string * string * mixfix) list -> theory -> theory
- val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
- val add_trfuns:
- (string * (ast list -> ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (ast list -> ast)) list -> theory -> theory
- val add_trrules: xrule list -> theory -> theory
- val add_axioms: (string * string) list -> theory -> theory
- val add_axioms_i: (string * term) list -> theory -> theory
- val add_thyname: string -> theory -> theory
-
-
-Appendix B: The |> operator
----------------------------
-
-Isabelle now provides an ML infix operator for reverse function application:
-
- infix |>;
- fun (x |> f) = f x;
-
-Using this, theory extension really becomes a pleasure, e.g.:
-
- FOL.thy
- |> add_consts
- [("nand", "[o, o] => o", NoSyn),
- ("#", "[o, o] => o", Infixl 30)]
- |> add_axioms
- [("nand_def", "nand(P, Q) == ~(P & Q)"),
- ("xor_def", "P # Q == P & ~Q | ~P & Q")]
- |> add_thyname "Gate";
-
-For a real-world example simply reset delete_tmpfiles, use_thy your favourite
-theory definition file and inspect the generated .XXX.thy.ML file.
-
-=============================================================================