src/HOL/Induct/Com.ML

 val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
 
 AddSEs exec_elim_cases;
 
 (*This theorem justifies using "exec" in the inductive definition of "eval"*)
-Goalw exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
+Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "exec_mono";
 
 
 Unify.trace_bound := 30;
 Unify.search_bound := 60;
 
 (*Command execution is functional (deterministic) provided evaluation is*)
-Goal "!!x. Function ev ==> Function(exec ev)";
+Goal "Function ev ==> Function(exec ev)";
 by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (etac exec.induct 1);
 by (Blast_tac 3);

 
 Goalw [assign_def] "(s[v/x])x = v";
 by (Simp_tac 1);
 qed "assign_same";
 
-Goalw [assign_def] "!!y. y~=x ==> (s[v/x])y = s y";
+Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
 by (Asm_simp_tac 1);
 qed "assign_different";
 
 Goalw [assign_def] "s[s x/x] = s";
 by (rtac ext 1);