The text for most sessions in chapter 4 appears below, where the sessions in the tutorial are enclosed in boxes and labelled in the upper right hand corner.

Session 1

- val th1 = BOOL_CASES_AX;
val th1 = |- !t. (t = T) \/ (t = F) : thm
- val th2 = SPEC (--`1=2`--) th1;
val th2 = |- ((1 = 2) = T) \/ ((1 = 2) = F) : thm

Session 2

- SPEC (--`1=2`--) th2;

uncaught exception HOL_ERR
- SPEC (--`1`--) th1;

uncaught exception HOL_ERR

Session 3

- val th3 = ASSUME (--`t1 ==> t2`--);
val th3 = . |- t1 ==> t2 : thm
- dest_thm th3;
val it = ([(--`t1 ==> t2`--)],(--`t1 ==> t2`--)) : term list * term

Session 4

- val th4 = DISCH (--`t1=>t2`--) th3;
HOL parser error: syntax error

Exception raised at Parse.first pass of parsing:
syntax error

uncaught exception HOL_ERR
- val th4 = DISCH (--`t1==>t2`--) th3;
val th4 = |- (t1 ==> t2) ==> t1 ==> t2 : thm

Session 5

- DISCH (--`1=2`--) th3;
val it = . |- (1 = 2) ==> t1 ==> t2 : thm
- dest_thm it;
val it = ([(--`t1 ==> t2`--)],(--`(1 = 2) ==> t1 ==> t2`--)) : term list * term

Session 6

- val th5 = ASSUME (--`t1`--);
Unconstrained type variable in the variable
   (t1 :?1)

Exception raised at Preterm.typecheck_cleanup:

uncaught exception HOL_ERR
- val th5 = ASSUME (--`t1:bool`--);
val th5 = . |- t1 : thm
- val th6 = MP th3 th5;
val th6 = .. |- t2 : thm

Session 7

- hyp th6;
val it = [(--`t1 ==> t2`--),(--`t1`--)] : term list

Session 8

- Globals.show_assums := true;
val it = () : unit
- th5;
val it = [t1] |- t1 : thm
- th6;
val it = [t1 ==> t2, t1] |- t2 : thm
Note: typing "open Globals;" (no quotation marks) will give you a list of assignable flags in the system.

Session 9

- val th7 = DISCH (--`t1==>t2`--) th6;
val th7 = [t1] |- (t1 ==> t2) ==> t2 : thm
- val th8 = DISCH (--`t1:bool`--) th7;
val th8 = |- t1 ==> (t1 ==> t2) ==> t2 : thm

Session 10

val th9 = [t3] |- t3 : thm
- val th10 = DISCH (--`t3:bool`--) th6;
val th10 = [t1 ==> t2, t1] |- t3 ==> t2 : thm
- val th11 = MP th10 th9;
val th11 = [t1, t1 ==> t2, t3] |- t2 : thm

Session 11

- fun ADD_ASSUM t th =
= let val th9 = ASSUME t
= in
= let val th10 = DISCH t th
= in
= MP th10 th9
= end
= end
= ;
val ADD_ASSUM = fn : term -> thm -> thm
- ADD_ASSUM (--`t3:bool`--) th6;
val it = [t1, t1 ==> t2, t3] |- t2 : thm

Session 12

- fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t);
val ADD_ASSUM = fn : term -> thm -> thm
- ADD_ASSUM (--`t3:bool`--) th6;
val it = [t1, t1 ==> t2, t3] |- t2 : thm

Session 13

- fun UNDISCH th =
= MP th (ASSUME(#ant(dest_imp(concl th))));
val UNDISCH = fn : thm -> thm
- th10;
val it = [t1 ==> t2, t1] |- t3 ==> t2 : thm
- UNDISCH th10;
val it = [t1, t1 ==> t2, t3] |- t2 : thm
- it = th11;
val it = true : bool

Session 14

HOL90 does not autoload libraries. In order to load the arithmetic library into a HOL90 session, type
      add_theory_to_sml "arithmetic"; 
Information about libraries in HOL90 can be found in doc/library.doc in the distribution. The names of the pre-existing theories can be found by looking in theories/ascii in the distribution.
- val rewrite_list = [ADD_CLAUSES,MULT_CLAUSES];
val rewrite_list =
  [|- (0 + m = m) /\
      (m + 0 = m) /\
      (SUC m + n = SUC (m + n)) /\
      (m + SUC n = SUC (m + n)),
   |- !m n.
        (0 * m = 0) /\
        (m * 0 = 0) /\
        (1 * m = m) /\
        (m * 1 = m) /\
        (SUC m * n = m * n + n) /\
        (m * SUC n = m + m * n)] : thm list

Session 15

- REWRITE_RULE rewrite_list (ASSUME (--`(m+0)<(1*n)+(SUC 0)`--));
val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm

Session 16

- add_theory_to_sml "prim_rec";
val num_Axiom = |- !e f. ?!fn1. (fn1 0 = e) /\ (!n. fn1 (SUC n) = f (fn1 n) n)
  : thm
val PRE = |- (PRE 0 = 0) /\ (!m. PRE (SUC m) = m) : thm
val LESS_SUC_SUC = |- !m. m < SUC m /\ m < SUC (SUC m) : thm
val LESS_NOT_EQ = |- !m n. m < n ==> ~(m = n) : thm
val NOT_LESS_EQ = |- !m n. (m = n) ==> ~(m < n) : thm
val SUC_ID = |- !n. ~(SUC n = n) : thm
val EQ_LESS = |- !n. (SUC m = n) ==> m < n : thm
val LESS_0 = |- !n. 0 < SUC n : thm
val LESS_SUC_IMP = |- !m n. m < SUC n ==> ~(m = n) ==> m < n : thm
val LESS_THM = |- !m n. m < SUC n = (m = n) \/ m < n : thm
val LESS_SUC = |- !m n. m < n ==> m < SUC n : thm
val LESS_SUC_REFL = |- !n. n < SUC n : thm
val LESS_MONO = |- !m n. m < n ==> SUC m < SUC n : thm
val NOT_LESS_0 = |- !n. ~(n < 0) : thm
val SUC_LESS = |- !m n. SUC m < n ==> m < n : thm
val LESS_REFL = |- !n. ~(n < n) : thm
val INV_SUC_EQ = |- !m n. (SUC m = SUC n) = m = n : thm
val it = () : unit
- REWRITE_RULE rewrite_list (ASSUME (--`(m+0)<(1*n)+(SUC 0)`--));
val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm
- REWRITE_RULE [LESS_THM] it;
val it = [m + 0 < 1 * n + SUC 0] |- (m = n) \/ m < n : thm

Session 17

- REWRITE_RULE [] (ASSUME (--`(T /\ x) \/ F ==> F`--));
val it = [T /\ x \/ F ==> F] |- ~x : thm

Session 18

Haven't figured this one out yet.

Session 20

- HOLdir;
val it = ref "/usr/local/hol/hol90.6/" : string ref

Session 21

Haven't tried this yet.

Session 22

- load_library{lib = Sys_lib.taut_lib, theory = "foo"};
Read doc/library.doc in the documentation for more information as to what load_library does.

Session 23 - 24

Haven't figured these out yet.