--- a/doc-src/IsarImplementation/IsaMakefile Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/IsaMakefile Wed Oct 13 13:05:23 2010 +0100
@@ -19,13 +19,13 @@
## sessions
-Thy: $(LOG)/Pure-Thy.gz
+Thy: $(LOG)/HOL-Thy.gz
-$(LOG)/Pure-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \
+$(LOG)/HOL-Thy.gz: Thy/ROOT.ML Thy/Base.thy Thy/Integration.thy \
Thy/Isar.thy Thy/Local_Theory.thy Thy/Logic.thy Thy/Prelim.thy \
Thy/Proof.thy Thy/Syntax.thy Thy/Tactic.thy Thy/ML.thy \
Thy/ML_old.thy ../antiquote_setup.ML
- @$(USEDIR) Pure Thy
+ @$(USEDIR) HOL Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
@@ -33,4 +33,4 @@
## clean
clean:
- @rm -f $(LOG)/Pure-Thy.gz
+ @rm -f $(LOG)/HOL-Thy.gz
--- a/doc-src/IsarImplementation/Thy/Base.thy Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Base.thy Wed Oct 13 13:05:23 2010 +0100
@@ -1,5 +1,5 @@
theory Base
-imports Pure
+imports Main
uses "../../antiquote_setup.ML"
begin
--- a/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Wed Oct 13 13:05:23 2010 +0100
@@ -5,8 +5,6 @@
chapter {* Isar language elements *}
text {*
- %FIXME proper formal markup of methods!?
-
The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
consists of three main categories of language elements:
@@ -23,7 +21,7 @@
\item Proof \emph{methods} define a secondary language of mixed
forward-backward refinement steps involving facts and goals.
- Typical examples are @{method rule}, @{method unfold}, and @{text
+ Typical examples are @{method rule}, @{method unfold}, and @{method
simp}.
Methods can occur in certain well-defined parts of the Isar proof
@@ -103,7 +101,7 @@
\item @{ML Proof.simple_goal}~@{text "state"} returns the structured
Isar goal (if available) in the form seen by ``simple'' methods
- (like @{text simp} or @{text blast}). The Isar goal facts are
+ (like @{method simp} or @{method blast}). The Isar goal facts are
already inserted as premises into the subgoals, which are presented
individually as in @{ML Proof.goal}.
@@ -114,9 +112,9 @@
\item @{ML Proof.raw_goal}~@{text "state"} returns the structured
Isar goal (if available) in the raw internal form seen by ``raw''
- methods (like @{text induct}). This form is rarely appropriate for
- dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} should
- be used in most situations.
+ methods (like @{method induct}). This form is rarely appropriate
+ for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
+ should be used in most situations.
\item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"}
initializes a toplevel Isar proof state within a given context.
@@ -162,7 +160,7 @@
text %mlex {* The following example peeks at a certain goal configuration. *}
example_proof
- have "PROP A" and "PROP B" and "PROP C"
+ have A and B and C
ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
oops
@@ -228,13 +226,14 @@
\begin{enumerate}
- \item structured method with cases, e.g.\ @{text "induct"}
+ \item structured method with cases, e.g.\ @{method "induct"}
- \item regular method: strong emphasis on facts, e.g.\ @{text "rule"}
+ \item regular method: strong emphasis on facts, e.g.\ @{method "rule"}
- \item simple method: weak emphasis on facts, merely inserted into subgoals, e.g.\ @{text "simp"}
+ \item simple method: weak emphasis on facts, merely inserted into
+ subgoals, e.g.\ @{method "simp"}
- \item old-style tactic emulation, e.g. @{text "rule_tac"}
+ \item old-style tactic emulation, e.g. @{method "rule_tac"}
\begin{itemize}
--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Oct 13 13:05:23 2010 +0100
@@ -121,8 +121,8 @@
@{index_ML_type sort: "class list"} \\
@{index_ML_type arity: "string * sort list * sort"} \\
@{index_ML_type typ} \\
- @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
- @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
+ @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
+ @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@@ -149,13 +149,14 @@
\item @{ML_type typ} represents types; this is a datatype with
constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
- \item @{ML map_atyps}~@{text "f \<tau>"} applies the mapping @{text "f"}
- to all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text
- "\<tau>"}.
+ \item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text
+ "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in
+ @{text "\<tau>"}.
- \item @{ML fold_atyps}~@{text "f \<tau>"} iterates the operation @{text
- "f"} over all occurrences of atomic types (@{ML TFree}, @{ML TVar})
- in @{text "\<tau>"}; the type structure is traversed from left to right.
+ \item @{ML Term.fold_atyps}~@{text "f \<tau>"} iterates the operation
+ @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML
+ TVar}) in @{text "\<tau>"}; the type structure is traversed from left to
+ right.
\item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
@@ -354,10 +355,10 @@
\begin{mldecls}
@{index_ML_type term} \\
@{index_ML "op aconv": "term * term -> bool"} \\
- @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
- @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
- @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
- @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
+ @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
+ @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
+ @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
+ @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML fastype_of: "term -> typ"} \\
@@ -383,20 +384,20 @@
on type @{ML_type term}; raw datatype equality should only be used
for operations related to parsing or printing!
- \item @{ML map_types}~@{text "f t"} applies the mapping @{text
+ \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text
"f"} to all types occurring in @{text "t"}.
- \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
- "f"} over all occurrences of types in @{text "t"}; the term
+ \item @{ML Term.fold_types}~@{text "f t"} iterates the operation
+ @{text "f"} over all occurrences of types in @{text "t"}; the term
structure is traversed from left to right.
- \item @{ML map_aterms}~@{text "f t"} applies the mapping @{text "f"}
- to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
+ \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text
+ "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML
Const}) occurring in @{text "t"}.
- \item @{ML fold_aterms}~@{text "f t"} iterates the operation @{text
- "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML Free},
- @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
+ \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation
+ @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML
+ Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is
traversed from left to right.
\item @{ML fastype_of}~@{text "t"} determines the type of a
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Oct 13 13:05:23 2010 +0100
@@ -1081,8 +1081,8 @@
ML {* Binding.pos_of @{binding here} *}
-text {* \medskip That position can be also printed in a message as
- follows. *}
+text {* \medskip\noindent That position can be also printed in a
+ message as follows. *}
ML_command {*
writeln
--- a/doc-src/IsarImplementation/Thy/Proof.thy Wed Oct 13 11:15:15 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Wed Oct 13 13:05:23 2010 +0100
@@ -159,12 +159,8 @@
\end{description}
*}
-text %mlex {* The following example (in theory @{theory Pure}) shows
- how to work with fixed term and type parameters and with
- type-inference.
-*}
-
-typedecl foo -- {* some basic type for testing purposes *}
+text %mlex {* The following example shows how to work with fixed term
+ and type parameters and with type-inference. *}
ML {*
(*static compile-time context -- for testing only*)
@@ -178,11 +174,11 @@
val t1' = singleton (Variable.polymorphic ctxt1) t1;
(*term u enforces specific type assignment*)
- val u = Syntax.read_term ctxt1 "(x::foo) \<equiv> y";
+ val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y";
(*official declaration of u -- propagates constraints etc.*)
val ctxt2 = ctxt1 |> Variable.declare_term u;
- val t2 = Syntax.read_term ctxt2 "x"; (*x::foo is enforced*)
+ val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*)
*}
text {* In the above example, the starting context had been derived