random fixes in reference manuals:

- single instead of double semicolons (ML prompts); - double backticks instead of single quotes (terms). These are probably a legacy of old HOL implementations.
HOL-Theorem-Prover · Oct 15, 2014 · 6990428 · 6990428
1 parent 0e21ee0
commit 6990428
Show file tree

Hide file tree

Showing 6 changed files with 31 additions and 32 deletions.
diff --git a/help/Docfiles/Arith.is_prenex.doc b/help/Docfiles/Arith.is_prenex.doc
@@ -15,11 +15,11 @@ Never fails.
 
 \EXAMPLE
 {
-#is_prenex "!x. ?y. x \/ y";;
-true : bool
+- is_prenex ``!x. ?y. x \/ y``;
+> val it = true : bool
 
-#is_prenex "!x. x ==> (?y. x /\ y)";;
-false : bool
+- is_prenex ``!x. x ==> (?y. x /\ y)``;
+> val it = false : bool
 }
 \USES
 Useful for determining whether it is necessary to apply a prenex normaliser to

diff --git a/help/Docfiles/Arith.is_presburger.doc b/help/Docfiles/Arith.is_presburger.doc
@@ -24,17 +24,17 @@ Never fails.
 
 \EXAMPLE
 {
-#is_presburger "!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p";;
-true : bool
+- is_presburger ``!m n p. m < (2 * n) /\ (n + n) <= p ==> m < SUC p``;
+> val it = true : bool
 
-#is_presburger "!m n p q. m < (n * p) /\ (n * p) < q ==> m < q";;
-false : bool
+- is_presburger ``!m n p q. m < (n * p) /\ (n * p) < q ==> m < q``;
+> val it = false : bool
 
-#is_presburger "(m <= n) ==> !p. (m < SUC(n + p))";;
-true : bool
+- is_presburger ``(m <= n) ==> !p. (m < SUC(n + p))``;
+> val it = true : bool
 
-#is_presburger "(m + n) - m = n";;
-true : bool
+- is_presburger ``(m + n) - m = n``;
+> val it = true : bool
 }
 \USES
 Useful for determining whether a decision procedure for Presburger arithmetic

diff --git a/help/Docfiles/Theory.new_type.doc b/help/Docfiles/Theory.new_type.doc
@@ -19,17 +19,17 @@ the current theory.
 A non-definitional version of ZF set theory might declare a new type {set} and 
 start using it as follows:
 {
-   - new_theory"ZF";
+   - new_theory "ZF";
    <<HOL message: Created theory "ZF">>
    > val it = () : unit
 
-   - new_type("set", 0);;
+   - new_type ("set", 0);
    > val it = () : unit
 
    - new_constant ("mem", Type`:set->set->bool`);
    > val it = () : unit
 
-   - new_axiom("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
+   - new_axiom ("EXT", Term`(!z. mem z x = mem z y) ==> (x = y)`);
    > val it = |- (!z. mem z x = mem z y) ==> (x = y) : thm
 }
 

diff --git a/help/Docfiles/Thm.mk_oracle_thm.doc b/help/Docfiles/Thm.mk_oracle_thm.doc
@@ -54,7 +54,7 @@ of inference.
    - val SimonThm = mk_oracle_thm tag;
    > val SimonThm = fn : term list * term -> thm
 
-   - val th = SimonThm ([], Term `!x. x`);;
+   - val th = SimonThm ([], Term `!x. x`);
    > val th = |- !x. x : thm
 
    - val th1 = SPEC F th;
@@ -75,7 +75,6 @@ Tags accumulate in a manner similar to logical hypotheses.
    > val it = [oracles: Serena, SimonSays] [axioms: ] [] |- F /\ T : thm
 }
 
-
 \COMMENTS
 It is impossible to detach a tag from a theorem.
 

diff --git a/help/Docfiles/boolSyntax.new_binder.doc b/help/Docfiles/boolSyntax.new_binder.doc
@@ -24,10 +24,10 @@ Fails if the type does not correspond to the above pattern.
 \EXAMPLE
 {
    - new_theory "anorak";
-   () : unit
+   > val it = () : unit
 
-   - new_binder ("!!", (bool-->bool)-->bool);;
-   () : unit
+   - new_binder ("!!", (bool-->bool)-->bool);
+   > val it = () : unit
 
    - Term `!!x. T`;
    > val it = `!! x. T` : term

diff --git a/help/Docfiles/numLib.ARITH_CONV.doc b/help/Docfiles/numLib.ARITH_CONV.doc
@@ -58,34 +58,34 @@ A simple example containing a free variable:
 A more complex example with subtraction and universal quantifiers, and
 which is not initially in prenex normal form:
 {
-   #ARITH_CONV
-   # "!m p. p < m ==> !q r. (m < (p + q) + r) ==> ((m - p) < q + r)";;
-   |- (!m p. p < m ==> (!q r. m < ((p + q) + r) ==> (m - p) < (q + r))) = T
+   - ARITH_CONV
+     ``!m p. p < m ==> !q r. (m < (p + q) + r) ==> ((m - p) < q + r)``;
+   > val it = |- (!m p. p < m ==> (!q r. m < ((p + q) + r) ==> (m - p) < (q + r))) = T
 }
 Two examples with existential quantifiers:
 {
-   #ARITH_CONV "?m n. m < n";;
-   |- (?m n. m < n) = T
+   - ARITH_CONV ``?m n. m < n``;
+   > val it = |- (?m n. m < n) = T
 
-   #ARITH_CONV "?m n. (2 * m) + (3 * n) = 10";;
-   |- (?m n. (2 * m) + (3 * n) = 10) = T
+   - ARITH_CONV ``?m n. (2 * m) + (3 * n) = 10``;
+   > val it = |- (?m n. (2 * m) + (3 * n) = 10) = T
 }
 An instance of a universally quantified formula involving a conditional
 statement and subtraction:
 {
-   #ARITH_CONV
-   # "((p + 3) <= n) ==> (!m. ((m EXP 2 = 0) => (n - 1) | (n - 2)) > p)";;
-   |- (p + 3) <= n ==> (!m. ((m EXP 2 = 0) => n - 1 | n - 2) > p) = T
+   - ARITH_CONV
+     ``((p + 3) <= n) ==> (!m. ((m EXP 2 = 0) => (n - 1) | (n - 2)) > p)``;
+   > val it = |- (p + 3) <= n ==> (!m. ((m EXP 2 = 0) => n - 1 | n - 2) > p) = T
 }
 Failure due to mixing quantifiers:
 {
-   #ARITH_CONV "!m. ?n. m < n";;
+   - ARITH_CONV ``!m. ?n. m < n``;
    evaluation failed     ARITH_CONV -- formula not in the allowed subset
 }
 Failure because the truth of the formula relies on the fact that the
 variables cannot have fractional values:
 {
-   #ARITH_CONV "!m n. ~(SUC (2 * m) = 2 * n)";;
+   - ARITH_CONV ``!m n. ~(SUC (2 * m) = 2 * n)``;
    evaluation failed     ARITH_CONV -- cannot prove formula
 }
 \SEEALSO