--- a/src/HOL/Subst/UTerm.ML Mon Mar 28 16:19:56 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/Subst/UTerm.ML
- ID: $Id$
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Simple term structure for unifiation.
-Binary trees with leaves that are constants or variables.
-*)
-
-open UTerm;
-
-
-(**** vars_of lemmas ****)
-
-Goal "(v : vars_of(Var(w))) = (w=v)";
-by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
-qed "vars_var_iff";
-
-Goal "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
-by (induct_tac "t" 1);
-by (ALLGOALS Simp_tac);
-by (fast_tac HOL_cs 1);
-qed "vars_iff_occseq";
-
-
-(* Not used, but perhaps useful in other proofs *)
-Goal "M<:N --> vars_of(M) <= vars_of(N)";
-by (induct_tac "N" 1);
-by (ALLGOALS Asm_simp_tac);
-by (fast_tac set_cs 1);
-val occs_vars_subset = result();
-
-
-Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)";
-by (Blast_tac 1);
-val monotone_vars_of = result();
-
-Goal "finite(vars_of M)";
-by (induct_tac"M" 1);
-by (ALLGOALS Simp_tac);
-by (ftac finite_UnI 1);
-by (assume_tac 1);
-by (Asm_simp_tac 1);
-val finite_vars_of = result();