src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 26 21:08:32 2017 +0100
@@ -108,9 +108,9 @@
 
 val simp_thms1 =
   map mk_meta_eq
-    @{lemma "(~ True) = False" "(~ False) = True"
-        "(True --> P) = P" "(False --> P) = True"
-        "(P & True) = P" "(True & P) = P"
+    @{lemma "(\<not> True) = False" "(\<not> False) = True"
+        "(True \<longrightarrow> P) = P" "(False \<longrightarrow> P) = True"
+        "(P \<and> True) = P" "(True \<and> P) = P"
       by (fact simp_thms)+};
 
 val simp_thms2 =
@@ -420,7 +420,7 @@
       (mono RS (fp_def RS
         (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
 
-    val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI];
+    val rules = [refl, TrueI, @{lemma "\<not> False" by (rule notI)}, exI, conjI];
 
     val intrs = map_index (fn (i, intr) =>
       Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
@@ -451,7 +451,7 @@
     val intrs = map dest_intr intr_ts ~~ intr_names;
 
     val rules1 = [disjE, exE, FalseE];
-    val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}];
+    val rules2 = [conjE, FalseE, @{lemma "\<not> True \<Longrightarrow> R" by (rule notE [OF _ TrueI])}];
 
     fun prove_elim c =
       let