# HG changeset patch
# User nipkow
# Date 899456132 -7200
# Node ID 58d267fc8630bde3002c934259fe28f41ab9b33b
# Parent  6b995dad8a9d96a5b078f9c6f8f9acd3dd007885
Removed leading !! in goals

diff -r 6b995dad8a9d -r 58d267fc8630 src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Fri Jul 03 10:37:04 1998 +0200
+++ b/src/HOL/Subst/Subst.ML	Fri Jul 03 10:55:32 1998 +0200
@@ -120,8 +120,8 @@
 by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
 qed "comp_assoc";
 
-Goal "!!s. [| theta =$= theta1; sigma =$= sigma1|] ==> \
-             \       (theta <> sigma) =$= (theta1 <> sigma1)";
+Goal "[| theta =$= theta1; sigma =$= sigma1|] ==> \
+\     (theta <> sigma) =$= (theta1 <> sigma1)";
 by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1);
 qed "subst_cong";
 
@@ -134,7 +134,7 @@
 qed "Cons_trivial";
 
 
-Goal "!!s. q <> r =$= s ==>  t <| q <| r = t <| s";
+Goal "q <> r =$= s ==>  t <| q <| r = t <| s";
 by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1);
 qed "comp_subst_subst";
 
@@ -172,7 +172,7 @@
 qed_spec_mp "Var_in_srange";
 
 Goal 
-     "!!v. [| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
+     "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
 by (blast_tac (claset() addIs [Var_in_srange]) 1);
 qed "Var_elim";
 
@@ -195,7 +195,7 @@
 by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1);
 qed "dom_range_disjoint";
 
-Goal "!!u. ~ u <| s = u ==> (? x. x : sdom(s))";
+Goal "~ u <| s = u ==> (? x. x : sdom(s))";
 by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1);
 by (Blast_tac 1);
 qed "subst_not_empty";
diff -r 6b995dad8a9d -r 58d267fc8630 src/HOL/Subst/Unifier.ML
--- a/src/HOL/Subst/Unifier.ML	Fri Jul 03 10:37:04 1998 +0200
+++ b/src/HOL/Subst/Unifier.ML	Fri Jul 03 10:55:32 1998 +0200
@@ -23,8 +23,8 @@
 AddIffs [Unifier_Comb];
 
 Goal
-  "!!v. [| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
-\       Unifier ((v,r)#s) t u";
+  "[| 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";
 
@@ -52,7 +52,7 @@
 
 
 Goal
-     "!!v. ~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
+     "~ 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;
@@ -88,8 +88,8 @@
 AddSIs [Var_Idem];
 
 Goalw [Idem_def]
-  "!!r. [| Idem(r); Unifier s (t<|r) (u<|r) |]       \
-\       ==> Unifier (r <> s) (t <| r) (u <| 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";
 
diff -r 6b995dad8a9d -r 58d267fc8630 src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Fri Jul 03 10:37:04 1998 +0200
+++ b/src/HOL/Subst/Unify.ML	Fri Jul 03 10:55:32 1998 +0200
@@ -70,8 +70,8 @@
  * about term structure.
  *---------------------------------------------------------------------------*)
 Goalw [unifyRel_def,lex_prod_def, inv_image_def]
-     "!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
-    \      ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
+  "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
+\  ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
 by (asm_full_simp_tac (simpset() addsimps [measure_def, 
                           less_eq, inv_image_def,add_assoc]) 1);
 by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
@@ -88,7 +88,7 @@
  * 3, 4, and 6. 
  *---------------------------------------------------------------------------*)
 Goal
- "!!x. ~(Var x <: M) ==>        \
+ "~(Var x <: M) ==> \
 \   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
 \ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
 by (case_tac "Var x = M" 1);