author | paulson |
Mon, 27 Nov 2000 11:06:28 +0100 | |
changeset 10523 | 68105cf615fa |
parent 10522 | ed3964d1f1a4 |
child 10524 | 270b285d48ee |
--- a/src/HOL/Integ/IntDef.ML Mon Nov 27 10:38:43 2000 +0100 +++ b/src/HOL/Integ/IntDef.ML Mon Nov 27 11:06:28 2000 +0100 @@ -14,11 +14,6 @@ by (Blast_tac 1); qed "intrel_iff"; -Goalw [intrel_def] "(x,x): intrel"; -by (pair_tac "x" 1); -by (Blast_tac 1); -qed "intrel_refl"; - Goalw [intrel_def, equiv_def, refl_def, sym_def, trans_def] "equiv UNIV intrel"; by Auto_tac;