src/HOL/W0/Type.ML

 
 Addsimps [mgu_eq,mgu_mg,mgu_free];
 
 (* mgu does not introduce new type variables *)
 Goalw [new_tv_def] 
-      "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
+      "[|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
 \            new_tv n u";
 by (fast_tac (set_cs addDs [mgu_free]) 1);
 qed "mgu_new";
 
 (* application of id_subst does not change type expression *)

 by (Simp_tac 1);
 qed "free_tv_id_subst";
 Addsimps [free_tv_id_subst];
 
 Goalw [dom_def,cod_def,UNION_def,Bex_def]
-  "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
+  "[| v : free_tv(s n); v~=n |] ==> v : cod s";
 by (Simp_tac 1);
 by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
 by (assume_tac 2);
 by (rotate_tac 1 1);
 by (Asm_full_simp_tac 1);

 by (fast_tac (HOL_cs addIs [new_tv_le] addss simpset()) 1);
 qed_spec_mp "new_tv_list_le";
 Addsimps [lessI RS less_imp_le RS new_tv_list_le];
 
 Goal
-  "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
+  "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 by (rtac conjI 1);
 by (slow_tac (HOL_cs addIs [le_trans]) 1);
 by (safe_tac HOL_cs );
 by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1);

 qed "new_tv_subst_le";
 Addsimps [lessI RS less_imp_le RS new_tv_subst_le];
 
 (* new_tv property remains if a substitution is applied *)
 Goal
-  "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
+  "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_var";
 
 Goal
   "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";

 qed "new_tv_Suc_list";
 
 
 (* composition of substitutions preserves new_tv proposition *)
 Goal 
-     "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
+     "[| new_tv n (s::subst); new_tv n r |] ==> \
 \           new_tv n (($ r) o s)";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_comp_1";
 
 Goal
-     "!! n. [| new_tv n (s::subst); new_tv n r |] ==>  \ 
+     "[| new_tv n (s::subst); new_tv n r |] ==>  \ 
 \     new_tv n (%v.$ r (s v))";
 by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
 qed "new_tv_subst_comp_2";
 
 Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2];
 
 (* new type variables do not occur freely in a type structure *)
 Goalw [new_tv_def] 
-      "!!n. new_tv n ts ==> n~:(free_tv ts)";
+      "new_tv n ts ==> n~:(free_tv ts)";
 by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
 qed "new_tv_not_free_tv";
 Addsimps [new_tv_not_free_tv];
 
 Goal

 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Fun t1 t2 *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 qed_spec_mp "eq_free_eq_subst_te";
 
-Goal
-  "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
+Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
 by (list.induct_tac "ts" 1);
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
 by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1);
 qed_spec_mp "eq_subst_tel_eq_free";
 
-Goal
-  "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
+Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
 by (list.induct_tac "ts" 1); 
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
 by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (simpset())) 1);
 qed_spec_mp "eq_free_eq_subst_tel";
 
 (* some useful theorems *)
 Goalw [free_tv_subst] 
-      "!!v. v : cod s ==> v : free_tv s";
+      "v : cod s ==> v : free_tv s";
 by (fast_tac set_cs 1);
 qed "codD";
  
 Goalw [free_tv_subst,dom_def] 
-      "!! x. x ~: free_tv s ==> s x = TVar x";
+      "x ~: free_tv s ==> s x = TVar x";
 by (fast_tac set_cs 1);
 qed "not_free_impl_id";
 
-Goalw [new_tv_def] 
-      "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
+Goalw [new_tv_def] "[| new_tv n t; m:free_tv t |] ==> m<n";
 by (fast_tac HOL_cs 1 );
 qed "free_tv_le_new_tv";
 
-Goal
-     "free_tv (s (v::nat)) <= insert v (cod s)";
+Goal "free_tv (s (v::nat)) <= insert v (cod s)";
 by (expand_case_tac "v:dom s" 1);
 by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
 by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
 qed "free_tv_subst_var";
 
-Goal 
-     "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
+Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
 by (typ.induct_tac "t" 1);
 (* case TVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
 by (fast_tac (set_cs addss simpset()) 1);
 qed "free_tv_app_subst_te";     
 
-Goal 
-     "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
+Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
 by (list.induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
 by (cut_facts_tac [free_tv_app_subst_te] 1);