src/HOL/HOL.thy

   by (unfold if_def) blast
 
 lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
   apply (rule case_split [of Q])
    apply (subst if_P)
-    prefer 3 apply (subst if_not_P)
-     apply blast+
+    prefer 3 apply (subst if_not_P, blast+)
   done
 
 lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
-  apply (subst split_if)
-  apply blast
-  done
+by (subst split_if, blast)
 
 lemmas if_splits = split_if split_if_asm
 
 lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))"
   by (rule split_if)
 
 lemma if_cancel: "(if c then x else x) = x"
-  apply (subst split_if)
-  apply blast
-  done
+by (subst split_if, blast)
 
 lemma if_eq_cancel: "(if x = y then y else x) = x"
-  apply (subst split_if)
-  apply blast
-  done
+by (subst split_if, blast)
 
 lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
   -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
   by (rule split_if)
 
 lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
-  apply (subst split_if)
-  apply blast
+  apply (subst split_if, blast)
   done
 
 lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
 lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
 

   apply (rule ccontr)
   apply (erule_tac x = "%z. if z = x then y else f z" in allE)
   apply (erule impE)
   apply (rule allI)
   apply (rule_tac P = "xa = x" in case_split_thm)
-  apply (drule_tac [3] x = x in fun_cong)
-  apply simp_all
+  apply (drule_tac [3] x = x in fun_cong, simp_all)
   done
 
 text{*Needs only HOL-lemmas:*}
 lemma mk_left_commute:
   assumes a: "\<And>x y z. f (f x y) z = f x (f y z)" and

 lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   by (simp add: order_less_le)
 
 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
-  apply (simp add: order_less_le)
-  apply blast
+  apply (simp add: order_less_le, blast)
   done
 
 lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]
 
 lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y"

 lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)"
   by (simp add: order_less_le order_antisym)
 
 lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P"
   apply (drule order_less_not_sym)
-  apply (erule contrapos_np)
-  apply simp
+  apply (erule contrapos_np, simp)
   done
 
 
 text {* Transitivity. *}
 

 axclass linorder < order
   linorder_linear: "x <= y | y <= x"
 
 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   apply (simp add: order_less_le)
-  apply (insert linorder_linear)
-  apply blast
+  apply (insert linorder_linear, blast)
   done
 
 lemma linorder_cases [case_names less equal greater]:
     "((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P"
-  apply (insert linorder_less_linear)
-  apply blast
+  apply (insert linorder_less_linear, blast)
   done
 
 lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)"
   apply (simp add: order_less_le)
   apply (insert linorder_linear)

   apply (insert linorder_linear)
   apply (blast intro: order_antisym)
   done
 
 lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)"
-  apply (cut_tac x = x and y = y in linorder_less_linear)
-  apply auto
-  done
+by (cut_tac x = x and y = y in linorder_less_linear, auto)
 
 lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R"
-  apply (simp add: linorder_neq_iff)
-  apply blast
-  done
+by (simp add: linorder_neq_iff, blast)
 
 
 subsubsection "Min and max on (linear) orders"
 
 lemma min_same [simp]: "min (x::'a::order) x = x"