src/Pure/Pure.thy

   and "realizability" :: thy_decl
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
 abbrevs
+  "===>" = "===>"  (*prevent replacement of very long arrows*)
+  "--->" = "\<midarrow>\<rightarrow>"
   "default_sort" = ""
   "simproc_setup" = ""
   "hence" = ""
   "hence" = "then have"
   "thus" = ""