diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index e2a5277c3b..6690ead61b 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -52,14 +52,6 @@ inductive sum (A : Type u) (B : Type v)
 | inl {} : A → sum
 | inr {} : B → sum
 
-attribute [reducible]
-def sum.intro_left {A : Type u} (B : Type v) (a : A) : sum A B :=
-sum.inl a
-
-attribute [reducible]
-def sum.intro_right (A : Type u) {B : Type v} (b : B) : sum A B :=
-sum.inr b
-
 inductive or (a b : Prop) : Prop
 | inl {} : a → or
 | inr {} : b → or
diff --git a/library/init/function.lean b/library/init/function.lean
index efd39c2869..f743511789 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -11,12 +11,10 @@ notation f ` $ `:1 a:1 := f a
 universe variables u_a u_b u_c u_d u_e
 variables {A : Type u_a} {B : Type u_b} {C : Type u_c} {D : Type u_d} {E : Type u_a}
 
-attribute [inline, reducible]
-def function.comp (f : B → C) (g : A → B) : A → C :=
+@[inline, reducible] def function.comp (f : B → C) (g : A → B) : A → C :=
 λ x, f (g x)
 
-attribute [inline, reducible]
-def function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
+@[inline, reducible] def function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
   (f : Π {x : A} (y : B x), C y) (g : Π x, B x) : Π x, C (g x) :=
 λ x, f (g x)
 
@@ -25,41 +23,32 @@ infixr  ` ∘' `:80  := function.dcomp
 
 namespace function
 
-attribute [reducible]
-def comp_right (f : B → B → B) (g : A → B) : B → A → B :=
+@[reducible] def comp_right (f : B → B → B) (g : A → B) : B → A → B :=
 λ b a, f b (g a)
 
-attribute [reducible]
-def comp_left (f : B → B → B) (g : A → B) : A → B → B :=
+@[reducible] def comp_left (f : B → B → B) (g : A → B) : A → B → B :=
 λ a b, f (g a) b
 
-attribute [reducible]
-def on_fun (f : B → B → C) (g : A → B) : A → A → C :=
+@[reducible] def on_fun (f : B → B → C) (g : A → B) : A → A → C :=
 λ x y, f (g x) (g y)
 
-attribute [reducible]
-def combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
+@[reducible] def combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
   : A → B → E :=
 λ x y, op (f x y) (g x y)
 
-attribute [reducible]
-def const (B : Type u_b) (a : A) : B → A :=
+@[reducible] def const (B : Type u_b) (a : A) : B → A :=
 λ x, a
 
-attribute [reducible]
-def swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
+@[reducible] def swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
 λ y x, f x y
 
-attribute [reducible]
-def app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
+@[reducible] def app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
 f x
 
-attribute [reducible]
-def curry : (A × B → C) → A → B → C :=
+@[reducible] def curry : (A × B → C) → A → B → C :=
 λ f a b, f (a, b)
 
-attribute [reducible]
-def uncurry : (A → B → C) → (A × B → C) :=
+@[reducible] def uncurry : (A → B → C) → (A × B → C) :=
 λ f p, match p with (a, b) := f a b end
 
 theorem curry_uncurry (f : A → B → C) : curry (uncurry f) = f :=
@@ -83,15 +72,13 @@ theorem comp.right_id (f : A → B) : f ∘ id = f := rfl
 
 theorem comp_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := rfl
 
-attribute [reducible]
-def injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
+@[reducible] def injective (f : A → B) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
 
 theorem injective_comp {g : B → C} {f : A → B} (Hg : injective g) (Hf : injective f) :
   injective (g ∘ f) :=
 take a₁ a₂, assume Heq, Hf (Hg Heq)
 
-attribute [reducible]
-def surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
+@[reducible] def surjective (f : A → B) : Prop := ∀ b, ∃ a, f a = b
 
 theorem surjective_comp {g : B → C} {f : A → B} (Hg : surjective g) (Hf : surjective f) :
   surjective (g ∘ f) :=
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 872a944a3f..1062aac1db 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -8,8 +8,7 @@ import init.datatypes
 
 universe variables u v w
 
-attribute [reducible]
-def id {A : Type u} (a : A) : A := a
+@[reducible] def id {A : Type u} (a : A) : A := a
 
 def flip {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : B → A → C :=
 λ b a, f a b
@@ -18,8 +17,7 @@ def flip {A : Type u} {B : Type v} {C : Type w} (f : A → B → C) : B → A 
 
 def implies (a b : Prop) := a → b
 
-attribute [trans]
-lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
+@[trans] lemma implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
 assume hp, h₂ (h₁ hp)
 
 def trivial : true := ⟨⟩
@@ -27,8 +25,7 @@ def trivial : true := ⟨⟩
 def not (a : Prop) := a → false
 prefix `¬` := not
 
-attribute [inline]
-def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
+@[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
 false.rec b (h₂ h₁)
 
 lemma not.intro {a : Prop} (h : a → false) : ¬ a :=
@@ -60,8 +57,7 @@ false.rec c h
 lemma proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ :=
 rfl
 
-attribute [defeq]
-def id.def {A : Type u} (a : A) : id a = a := rfl
+@[defeq] def id.def {A : Type u} (a : A) : id a = a := rfl
 
 -- Remark: we provide the universe levels explicitly to make sure `eq.drec` has the same type of `eq.rec` in the hoTT library
 attribute [elab_as_eliminator]
@@ -117,8 +113,7 @@ section
   assume hp, h ▸ hp
 end
 
-attribute [inline]
-def cast {A B : Type u} (h : A = B) (a : A) : B :=
+@[inline] def cast {A B : Type u} (h : A = B) (a : A) : B :=
 eq.rec a h
 
 lemma cast_proof_irrel {A B : Type u} (h₁ h₂ : A = B) (a : A) : cast h₁ a = cast h₂ a :=
@@ -129,10 +124,9 @@ rfl
 
 /- ne -/
 
-attribute [reducible]
-def ne {A : Type u} (a b : A) := ¬(a = b)
-attribute [defeq]
-def ne.def {A : Type u} (a b : A) : ne a b = ¬ (a = b) := rfl
+@[reducible] def ne {A : Type u} (a b : A) := ¬(a = b)
+
+@[defeq] def ne.def {A : Type u} (a b : A) : ne a b = ¬ (a = b) := rfl
 notation a ≠ b := ne a b
 
 namespace ne
@@ -638,14 +632,12 @@ is_false not_false
 
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
-attribute [inline]
-def dite (c : Prop) [h : decidable c] {A : Type u} : (c → A) → (¬ c → A) → A :=
+@[inline] def dite (c : Prop) [h : decidable c] {A : Type u} : (c → A) → (¬ c → A) → A :=
 λ t e, decidable.rec_on h e t
 
 /- if-then-else -/
 
-attribute [inline]
-def ite (c : Prop) [h : decidable c] {A : Type u} (t e : A) : A :=
+@[inline] def ite (c : Prop) [h : decidable c] {A : Type u} (t e : A) : A :=
 decidable.rec_on h (λ hnc, e) (λ hc, t)
 
 namespace decidable
@@ -713,12 +705,9 @@ section
   and.decidable
 end
 
-attribute [reducible]
-def decidable_pred {A : Type u} (r : A → Prop) := Π (a   : A), decidable (r a)
-attribute [reducible]
-def decidable_rel  {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
-attribute [reducible]
-def decidable_eq   (A : Type u) := decidable_rel (@eq A)
+@[reducible] def decidable_pred {A : Type u} (r : A → Prop) := Π (a : A), decidable (r a)
+@[reducible] def decidable_rel  {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
+@[reducible] def decidable_eq   (A : Type u) := decidable_rel (@eq A)
 
 instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) :=
 implies.decidable
@@ -762,8 +751,7 @@ class inhabited (A : Type u) :=
 def default (A : Type u) [inhabited A] : A :=
 inhabited.default A
 
-attribute [inline, irreducible]
-def arbitrary (A : Type u) [inhabited A] : A :=
+@[inline, irreducible] def arbitrary (A : Type u) [inhabited A] : A :=
 default A
 
 instance prop.inhabited : inhabited Prop :=
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 6791288fa7..19ff81f84e 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -92,8 +92,7 @@ namespace nat
   protected definition le_refl : ∀ a : ℕ, a ≤ a :=
   le.nat_refl
 
-  attribute [reducible]
-  protected definition lt (n m : ℕ) := succ n ≤ m
+  @[reducible] protected definition lt (n m : ℕ) := succ n ≤ m
 
   instance : has_lt ℕ :=
   ⟨nat.lt⟩
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index b84fc8d798..abfae2cb64 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -128,6 +128,8 @@
   `((;; attributes
      (,(rx word-start "attribute" word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))))
       (1 'font-lock-doc-face))
+     (,(rx (group "@[" (zero-or-more (not (any "]"))) "]"))
+      (1 'font-lock-doc-face))
      ;; mutal definitions "names"
      (,(rx word-start
            "mutual"
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index f5ba31e4ee..69a4e8885d 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -15,10 +15,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 
 namespace lean {
-void decl_attributes::parse(parser & p) {
-    if (!p.curr_is_token(get_lbracket_tk()))
-        return;
-    p.next();
+void decl_attributes::parse_core(parser & p, bool compact) {
     while (true) {
         auto pos = p.pos();
         bool deleted = p.curr_is_token_or_id(get_sub_tk());
@@ -73,6 +70,8 @@ void decl_attributes::parse(parser & p) {
             p.next();
         } else {
             p.check_token_next(get_rbracket_tk(), "invalid attribute declaration, ']' expected");
+            if (compact)
+                break;
             if (p.curr_is_token(get_lbracket_tk()))
                 p.next();
             else
@@ -81,6 +80,17 @@ void decl_attributes::parse(parser & p) {
     }
 }
 
+void decl_attributes::parse(parser & p) {
+    if (!p.curr_is_token(get_lbracket_tk()))
+        return;
+    p.next();
+    parse_core(p, false);
+}
+
+void decl_attributes::parse_compact(parser & p) {
+    parse_core(p, true);
+}
+
 void decl_attributes::set_attribute(environment const & env, name const & attr_name) {
     if (!is_attribute(env, attr_name))
         throw exception(sstream() << "unknown attribute [" << attr_name << "]");
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index a6e1055bb8..a771811945 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -23,10 +23,14 @@ private:
     bool               m_parsing_only;
     list<entry>        m_entries;
     optional<unsigned> m_prio;
+    void parse_core(parser & p, bool compact);
 public:
     decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
     void set_attribute(environment const & env, name const & attr_name);
+    /* attributes: zero-or-more [ ... ] */
     void parse(parser & p);
+    /* Parse attributes after `@[` ... ] */
+    void parse_compact(parser & p);
     environment apply(environment env, io_state const & ios, name const & d) const;
     list<entry> const & get_entries() const { return m_entries; }
     bool is_parsing_only() const { return m_parsing_only; }
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 1399057d42..7d5a56fac1 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -527,6 +527,19 @@ environment local_attribute_cmd(parser & p) {
     return attribute_cmd_core(p, false);
 }
 
+static environment compact_attribute_cmd(parser & p) {
+    bool persistent = true;
+    decl_attributes attributes(persistent);
+    attributes.parse_compact(p);
+    if (p.curr_is_token_or_id(get_inductive_tk())) {
+        return inductive_cmd_ex(p, attributes);
+    } else  if (p.curr_is_token_or_id(get_structure_tk())) {
+        return structure_cmd_ex(p, attributes, false);
+    } else {
+        return definition_cmd_ex(p, attributes);
+    }
+}
+
 static environment include_cmd_core(parser & p, bool include) {
     if (!p.curr_is_identifier())
         throw parser_error(sstream() << "invalid include/omit command, identifier expected", p.pos());
@@ -591,6 +604,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("reveal",          "reveal given theorems", reveal_cmd));
     add_cmd(r, cmd_info("include",         "force section parameter/variable to be included", include_cmd));
     add_cmd(r, cmd_info("attribute",       "set declaration attributes", attribute_cmd));
+    add_cmd(r, cmd_info("@[",              "declaration attributes", compact_attribute_cmd));
     add_cmd(r, cmd_info("omit",            "undo 'include' command", omit_cmd));
 }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index f633573be0..3d3459438e 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -100,20 +100,15 @@ void init_token_table(token_table & t) {
 
     char const * commands[] =
         {"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
-         "definition", "meta", "mutual",
-         "example", "coercion", "noncomputable",
+         "definition", "meta", "mutual", "example", "coercion", "noncomputable",
          "variables", "parameter", "parameters", "constant", "constants",
-         "[visible]", "[none]",
-         "evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]", "[unfold_hints]",
+         "evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]",
          "print", "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "class", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
-         "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation",
-         "exit", "set_option", "open", "export", "override", "tactic_hint",
-         "add_begin_end_tactic", "set_begin_end_tactic",
-         "multiple_instances", "find_decl", "attribute", "persistent", "instance",
-         "include", "omit", "migrate",
-         "init_quotient", "init_hits", "declare_trace", "register_simp_ext",
+         "exit", "set_option", "open", "export", "override", "@[",
+         "attribute", "persistent", "instance", "include", "omit", "init_quotient",
+         "init_hits", "declare_trace", "register_simp_ext",
          "run_command", "add_key_equivalence", "#erase_cache",
          "#compile", "#unify", nullptr};
 
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index a1db343355..a226d38e12 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -19,8 +19,6 @@ static name const * g_lcurly_tk = nullptr;
 static name const * g_rcurly_tk = nullptr;
 static name const * g_ldcurly_tk = nullptr;
 static name const * g_rdcurly_tk = nullptr;
-static name const * g_lcurlybar_tk = nullptr;
-static name const * g_rcurlybar_tk = nullptr;
 static name const * g_lbracket_tk = nullptr;
 static name const * g_rbracket_tk = nullptr;
 static name const * g_langle_tk = nullptr;
@@ -69,7 +67,6 @@ static name const * g_renaming_tk = nullptr;
 static name const * g_replacing_tk = nullptr;
 static name const * g_extends_tk = nullptr;
 static name const * g_as_tk = nullptr;
-static name const * g_none_tk = nullptr;
 static name const * g_whnf_tk = nullptr;
 static name const * g_in_tk = nullptr;
 static name const * g_assign_tk = nullptr;
@@ -138,8 +135,6 @@ void initialize_tokens() {
     g_rcurly_tk = new name{"}"};
     g_ldcurly_tk = new name{"⦃"};
     g_rdcurly_tk = new name{"⦄"};
-    g_lcurlybar_tk = new name{"{|"};
-    g_rcurlybar_tk = new name{"|}"};
     g_lbracket_tk = new name{"["};
     g_rbracket_tk = new name{"]"};
     g_langle_tk = new name{"⟨"};
@@ -188,7 +183,6 @@ void initialize_tokens() {
     g_replacing_tk = new name{"replacing"};
     g_extends_tk = new name{"extends"};
     g_as_tk = new name{"as"};
-    g_none_tk = new name{"[none]"};
     g_whnf_tk = new name{"[whnf]"};
     g_in_tk = new name{"in"};
     g_assign_tk = new name{":="};
@@ -258,8 +252,6 @@ void finalize_tokens() {
     delete g_rcurly_tk;
     delete g_ldcurly_tk;
     delete g_rdcurly_tk;
-    delete g_lcurlybar_tk;
-    delete g_rcurlybar_tk;
     delete g_lbracket_tk;
     delete g_rbracket_tk;
     delete g_langle_tk;
@@ -308,7 +300,6 @@ void finalize_tokens() {
     delete g_replacing_tk;
     delete g_extends_tk;
     delete g_as_tk;
-    delete g_none_tk;
     delete g_whnf_tk;
     delete g_in_tk;
     delete g_assign_tk;
@@ -377,8 +368,6 @@ name const & get_lcurly_tk() { return *g_lcurly_tk; }
 name const & get_rcurly_tk() { return *g_rcurly_tk; }
 name const & get_ldcurly_tk() { return *g_ldcurly_tk; }
 name const & get_rdcurly_tk() { return *g_rdcurly_tk; }
-name const & get_lcurlybar_tk() { return *g_lcurlybar_tk; }
-name const & get_rcurlybar_tk() { return *g_rcurlybar_tk; }
 name const & get_lbracket_tk() { return *g_lbracket_tk; }
 name const & get_rbracket_tk() { return *g_rbracket_tk; }
 name const & get_langle_tk() { return *g_langle_tk; }
@@ -427,7 +416,6 @@ name const & get_renaming_tk() { return *g_renaming_tk; }
 name const & get_replacing_tk() { return *g_replacing_tk; }
 name const & get_extends_tk() { return *g_extends_tk; }
 name const & get_as_tk() { return *g_as_tk; }
-name const & get_none_tk() { return *g_none_tk; }
 name const & get_whnf_tk() { return *g_whnf_tk; }
 name const & get_in_tk() { return *g_in_tk; }
 name const & get_assign_tk() { return *g_assign_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index d076d65582..3c335a6109 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -21,8 +21,6 @@ name const & get_lcurly_tk();
 name const & get_rcurly_tk();
 name const & get_ldcurly_tk();
 name const & get_rdcurly_tk();
-name const & get_lcurlybar_tk();
-name const & get_rcurlybar_tk();
 name const & get_lbracket_tk();
 name const & get_rbracket_tk();
 name const & get_langle_tk();
@@ -71,7 +69,6 @@ name const & get_renaming_tk();
 name const & get_replacing_tk();
 name const & get_extends_tk();
 name const & get_as_tk();
-name const & get_none_tk();
 name const & get_whnf_tk();
 name const & get_in_tk();
 name const & get_assign_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 74b33c6910..fb0b41e807 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -14,8 +14,6 @@ lcurly       {
 rcurly       }
 ldcurly      ⦃
 rdcurly      ⦄
-lcurlybar    {|
-rcurlybar    |}
 lbracket     [
 rbracket     ]
 langle       ⟨
@@ -64,7 +62,6 @@ renaming     renaming
 replacing    replacing
 extends      extends
 as           as
-none         [none]
 whnf         [whnf]
 in           in
 assign       :=