equal
deleted
inserted
replaced
6 (*Unfold all "let"s involving constants*) |
6 (*Unfold all "let"s involving constants*) |
7 Goalw [Let_def] "Let (number_of v) f == f (number_of v)"; |
7 Goalw [Let_def] "Let (number_of v) f == f (number_of v)"; |
8 by(Simp_tac 1); |
8 by(Simp_tac 1); |
9 qed "Let_number_of"; |
9 qed "Let_number_of"; |
10 Addsimps [Let_number_of]; |
10 Addsimps [Let_number_of]; |
|
11 |
|
12 (*The condition "True" is a hack to prevent looping. |
|
13 Conditional rewrite rules are tried after unconditional ones, so a rule |
|
14 like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) |
|
15 Goal "True ==> (number_of w = x) = (x = number_of w)"; |
|
16 by Auto_tac; |
|
17 qed "number_of_reorient"; |
|
18 Addsimps [number_of_reorient]; |