3 let max_real_symm = prove_by_refinement(
4 `!a b. max_real a b = max_real b a`,
9 USE 0 (MATCH_MP (REAL_ARITH `a < b ==> ~(b < a)`));
19 let SIGMAHAT_EQ = prove(
20 `!x1 x2 x3 x4 x5 x6. sigmahat_x x1 x2 x3 x4 x5 x6 = sigmahat_x' x1 x2 x3 x4 x5 x6`,
22 REWRITE_TAC [sigmahat_x';sigmahat_x] THEN
35 COND_CASES_TAC THEN REWRITE_TAC[] THEN
36 COND_CASES_TAC THEN REWRITE_TAC[] THEN
38 COND_CASES_TAC THEN REWRITE_TAC[] THEN
40 COND_CASES_TAC THEN REWRITE_TAC[] THEN
42 COND_CASES_TAC THEN REWRITE_TAC[] THEN
45 ONCE_REWRITE_TAC[MAX_REAL_SYMM]
48 let TEST = prove(`!x:bool. x = x`,
54 (program-get-line) let x = 5
58 e (REWRITE_TAC[sigmahat_sean_x;sigmahat_x;LET_DEF;LET_END_DEF])
59 e (REPEAT COND_CASES_TAC THEN REWRITE_TAC[])