src/HOL/Subst/Unify.ML
changeset 5069 3ea049f7979d
parent 4686 74a12e86b20b
child 5119 58d267fc8630
     1.1 --- a/src/HOL/Subst/Unify.ML	Mon Jun 22 17:13:09 1998 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Mon Jun 22 17:26:46 1998 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4   * Termination proof.
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 -goalw Unify.thy [unifyRel_def, measure_def] "trans unifyRel";
     1.8 +Goalw [unifyRel_def, measure_def] "trans unifyRel";
     1.9  by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, 
    1.10  			 trans_finite_psubset, trans_less_than,
    1.11  			 trans_inv_image] 1));
    1.12 @@ -69,7 +69,7 @@
    1.13   * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
    1.14   * about term structure.
    1.15   *---------------------------------------------------------------------------*)
    1.16 -goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
    1.17 +Goalw [unifyRel_def,lex_prod_def, inv_image_def]
    1.18       "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
    1.19      \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
    1.20  by (asm_full_simp_tac (simpset() addsimps [measure_def, 
    1.21 @@ -87,7 +87,7 @@
    1.22   * This lemma proves the nested termination condition for the base cases 
    1.23   * 3, 4, and 6. 
    1.24   *---------------------------------------------------------------------------*)
    1.25 -goal Unify.thy
    1.26 +Goal
    1.27   "!!x. ~(Var x <: M) ==>        \
    1.28  \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
    1.29  \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
    1.30 @@ -175,7 +175,7 @@
    1.31   *---------------------------------------------------------------------------*)
    1.32  
    1.33  (*Desired rule, copied from the theory file.  Could it be made available?*)
    1.34 -goal Unify.thy 
    1.35 +Goal 
    1.36    "unify(Comb M1 N1, Comb M2 N2) =      \
    1.37  \      (case unify(M1,M2)               \
    1.38  \        of None => None                \
    1.39 @@ -204,7 +204,7 @@
    1.40   * approach of M&W, who used idempotence and MGU-ness in the termination proof.
    1.41   *---------------------------------------------------------------------------*)
    1.42  
    1.43 -goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
    1.44 +Goal "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
    1.45  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.46  by (ALLGOALS Asm_simp_tac);
    1.47  (*Const-Const case*)
    1.48 @@ -240,7 +240,7 @@
    1.49  (*---------------------------------------------------------------------------
    1.50   * Unify returns idempotent substitutions, when it succeeds.
    1.51   *---------------------------------------------------------------------------*)
    1.52 -goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
    1.53 +Goal "!theta. unify(M,N) = Some theta --> Idem theta";
    1.54  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.55  by (ALLGOALS 
    1.56      (asm_simp_tac