src/HOL/Subst/Unify.ML
changeset 3241 91b543ab091b
parent 3209 ccb55f3121d1
child 3266 89e5f4163663
     1.1 --- a/src/HOL/Subst/Unify.ML	Tue May 20 11:41:56 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Tue May 20 11:42:59 1997 +0200
     1.3 @@ -70,21 +70,10 @@
     1.4   * Termination proof.
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 -goalw Unify.thy [trans_def,inv_image_def]
     1.8 -    "!!r. trans r ==> trans (inv_image r f)";
     1.9 -by (Simp_tac 1);
    1.10 -by (Blast_tac 1);
    1.11 -qed "trans_inv_image";
    1.12 -
    1.13 -goalw Unify.thy [finite_psubset_def, trans_def] "trans finite_psubset";
    1.14 -by (simp_tac (!simpset addsimps [psubset_def]) 1);
    1.15 -by (Blast_tac 1);
    1.16 -qed "trans_finite_psubset";
    1.17 -
    1.18  goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
    1.19 -by (REPEAT (resolve_tac [trans_inv_image,trans_lex_prod,conjI, 
    1.20 -			 trans_finite_psubset,
    1.21 -			 trans_rprod, trans_inv_image, trans_trancl] 1));
    1.22 +by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, 
    1.23 +			 trans_finite_psubset, trans_less_than,
    1.24 +			 trans_rprod, trans_inv_image] 1));
    1.25  qed "trans_unifyRel";
    1.26  
    1.27  
    1.28 @@ -169,7 +158,7 @@
    1.29   * The nested TC. Proved by recursion induction.
    1.30   *---------------------------------------------------------------------------*)
    1.31  val [tc1,tc2,tc3] = unify.tcs;
    1.32 -goalw_cterm [] (cterm_of (sign_of Unify.thy) (USyntax.mk_prop tc3));
    1.33 +goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
    1.34  (*---------------------------------------------------------------------------
    1.35   * The extracted TC needs the scope of its quantifiers adjusted, so our 
    1.36   * first step is to restrict the scopes of N1 and N2.