src/HOL/Subst/Unifier.ML

 
 (*---------------------------------------------------------------------------
  * Unifiers 
  *---------------------------------------------------------------------------*)
 
-goal Unifier.thy
+Goal
     "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
 by (simp_tac (simpset() addsimps [Unifier_def]) 1);
 qed "Unifier_Comb";
 
 AddIffs [Unifier_Comb];
 
-goal Unifier.thy
+Goal
   "!!v. [| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
 \       Unifier ((v,r)#s) t u";
 by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1);
 qed "Cons_Unifier";
 
 
 (*---------------------------------------------------------------------------
  * Most General Unifiers 
  *---------------------------------------------------------------------------*)
 
-goalw Unifier.thy unify_defs "MGUnifier s t u = MGUnifier s u t";
+Goalw unify_defs "MGUnifier s t u = MGUnifier s u t";
 by (blast_tac (claset() addIs [sym]) 1);
 qed "mgu_sym";
 
 
-goal Unifier.thy  "[] >> s";
+Goal  "[] >> s";
 by (simp_tac (simpset() addsimps [MoreGeneral_def]) 1);
 by (Blast_tac 1);
 qed "MoreGen_Nil";
 
 AddIffs [MoreGen_Nil];
 
-goalw Unifier.thy unify_defs
+Goalw unify_defs
     "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)";
 by (auto_tac (claset() addIs [ssubst_subst2, subst_comp_Nil], simpset()));
 qed "MGU_iff";
 
 
-goal Unifier.thy
+Goal
      "!!v. ~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
 by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
 	              delsimps [subst_Var]) 1);
 by Safe_tac;
 by (rtac exI 1);

 
 (*---------------------------------------------------------------------------
  * Idempotence.
  *---------------------------------------------------------------------------*)
 
-goalw Unifier.thy [Idem_def] "Idem([])";
+Goalw [Idem_def] "Idem([])";
 by (Simp_tac 1);
 qed "Idem_Nil";
 
 AddIffs [Idem_Nil];
 
-goalw Unifier.thy [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
+Goalw [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
 by (simp_tac (simpset() addsimps [subst_eq_iff, invariance, 
 				 dom_range_disjoint]) 1);
 qed "Idem_iff";
 
-goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
+Goal "~ (Var(v) <: t) --> Idem([(v,t)])";
 by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
 				  empty_iff_all_not]) 1);
 qed_spec_mp "Var_Idem";
 
 AddSIs [Var_Idem];
 
-goalw Unifier.thy [Idem_def]
+Goalw [Idem_def]
   "!!r. [| Idem(r); Unifier s (t<|r) (u<|r) |]       \
 \       ==> Unifier (r <> s) (t <| r) (u <| r)";
 by (asm_full_simp_tac (simpset() addsimps [Unifier_def, comp_subst_subst]) 1);
 qed "Unifier_Idem_subst";