# HG changeset patch
# User wenzelm
# Date 1470157129 -7200
# Node ID 71ee1b8067ccc663af53e1b8e3dd3f164e3f1334
# Parent  a4acecf4dc21a4e2d8992cc9a03303ebcaa3d3b4# Parent  f4a308fdf6647a2ef203890264f22b287186eede
merged

diff -r a4acecf4dc21 -r 71ee1b8067cc NEWS
--- a/NEWS	Tue Aug 02 13:13:15 2016 +0200
+++ b/NEWS	Tue Aug 02 18:58:49 2016 +0200
@@ -111,6 +111,12 @@
 * Completion templates for commands involving "begin ... end" blocks,
 e.g. 'context', 'notepad'.
 
+* Additional abbreviations for syntactic completion may be specified
+within the theory header as 'abbrevs', in addition to global
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
+before. The theory syntax for 'keywords' has been simplified
+accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+
 
 *** Isar ***
 
diff -r a4acecf4dc21 -r 71ee1b8067cc etc/abbrevs
--- a/etc/abbrevs	Tue Aug 02 13:13:15 2016 +0200
+++ b/etc/abbrevs	Tue Aug 02 18:58:49 2016 +0200
@@ -4,7 +4,3 @@
 "===>" = "===>"
 
 "--->" = "\<midarrow>\<rightarrow>"
-
-(*HOL-NSA*)
-"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
-"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -58,14 +58,14 @@
   such a global @{command (global) "end"}.
 
   @{rail \<open>
-    @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
-    ;
-    imports: @'imports' (@{syntax name} +)
+    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
+      keywords? abbrevs? @'begin'
     ;
     keywords: @'keywords' (keyword_decls + @'and')
     ;
-    keyword_decls: (@{syntax string} +)
-      ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
+    keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
+    ;
+    abbrevs: @'abbrevs' ((text '=' text) +)
     ;
     @@{command thy_deps} (thy_bounds thy_bounds?)?
     ;
@@ -85,7 +85,7 @@
   based on Isabelle. Regular user theories usually refer to some more complex
   entry point, such as theory @{theory Main} in Isabelle/HOL.
 
-  The optional @{keyword_def "keywords"} specification declares outer syntax
+  The @{keyword_def "keywords"} specification declares outer syntax
   (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare
   in end-user applications). Both minor keywords and major keywords of the
   Isar command language need to be specified, in order to make parsing of
@@ -97,8 +97,10 @@
   @{syntax tags} provide defaults for document preparation
   (\secref{sec:tags}).
 
-  It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while
-  the default is the corresponding keyword name.
+  The @{keyword_def "abbrevs"} specification declares additional abbreviations
+  for syntactic completion. The default for a new keyword is just its name,
+  but completion may be avoided by defining @{keyword "abbrevs"} with empty
+  text.
   
   \<^descr> @{command (global) "end"} concludes the current theory definition. Note
   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Basic logical reasoning\<close>
 
 theory Basic_Logic
-imports Main
+  imports Main
 begin
 
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Cantor's Theorem\<close>
 
 theory Cantor
-imports Main
+  imports Main
 begin
 
 subsection \<open>Mathematical statement and proof\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>The Drinker's Principle\<close>
 
 theory Drinker
-imports Main
+  imports Main
 begin
 
 text \<open>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Correctness of a simple expression compiler\<close>
 
 theory Expr_Compiler
-imports Main
+  imports Main
 begin
 
 text \<open>
@@ -46,10 +46,10 @@
 \<close>
 
 primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
-where
-  "eval (Variable x) env = env x"
-| "eval (Constant c) env = c"
-| "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+  where
+    "eval (Variable x) env = env x"
+  | "eval (Constant c) env = c"
+  | "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
 
 
 subsection \<open>Machine\<close>
@@ -69,14 +69,13 @@
 \<close>
 
 primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
-where
-  "exec [] stack env = stack"
-| "exec (instr # instrs) stack env =
-    (case instr of
-      Const c \<Rightarrow> exec instrs (c # stack) env
-    | Load x \<Rightarrow> exec instrs (env x # stack) env
-    | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
-                   # (tl (tl stack))) env)"
+  where
+    "exec [] stack env = stack"
+  | "exec (instr # instrs) stack env =
+      (case instr of
+        Const c \<Rightarrow> exec instrs (c # stack) env
+      | Load x \<Rightarrow> exec instrs (env x # stack) env
+      | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)"
 
 definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
   where "execute instrs env = hd (exec instrs [] env)"
@@ -90,10 +89,10 @@
 \<close>
 
 primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
-where
-  "compile (Variable x) = [Load x]"
-| "compile (Constant c) = [Const c]"
-| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+  where
+    "compile (Variable x) = [Load x]"
+  | "compile (Constant c) = [Const c]"
+  | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
 
 
 text \<open>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -15,7 +15,7 @@
 section \<open>Fib and Gcd commute\<close>
 
 theory Fibonacci
-imports "../Number_Theory/Primes"
+  imports "../Number_Theory/Primes"
 begin
 
 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
@@ -28,10 +28,10 @@
 subsection \<open>Fibonacci numbers\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
-where
-  "fib 0 = 0"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+  where
+    "fib 0 = 0"
+  | "fib (Suc 0) = 1"
+  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 lemma [simp]: "fib (Suc n) > 0"
   by (induct n rule: fib.induct) simp_all
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/First_Order_Logic.thy
--- a/src/HOL/Isar_Examples/First_Order_Logic.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/First_Order_Logic.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -10,7 +10,7 @@
 \<close>
 
 theory First_Order_Logic
-imports Pure
+  imports Pure
 begin
 
 subsection \<open>Abstract syntax\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Basic group theory\<close>
 
 theory Group
-imports Main
+  imports Main
 begin
 
 subsection \<open>Groups and calculational reasoning\<close> 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Group_Context.thy
--- a/src/HOL/Isar_Examples/Group_Context.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
 
 theory Group_Context
-imports Main
+  imports Main
 begin
 
 text \<open>hypothetical group axiomatization\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Group_Notepad.thy
--- a/src/HOL/Isar_Examples/Group_Notepad.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
 
 theory Group_Notepad
-imports Main
+  imports Main
 begin
 
 notepad
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Foundations of HOL\<close>
 
 theory Higher_Order_Logic
-imports Pure
+  imports Pure
 begin
 
 text \<open>
@@ -76,7 +76,8 @@
 
 subsubsection \<open>Derived connectives\<close>
 
-definition false :: o  ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
+definition false :: o  ("\<bottom>")
+  where "\<bottom> \<equiv> \<forall>A. A"
 
 theorem falseE [elim]:
   assumes "\<bottom>"
@@ -87,7 +88,8 @@
 qed
 
 
-definition true :: o  ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o  ("\<top>")
+  where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
 
 theorem trueI [intro]: \<top>
   unfolding true_def ..
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Hoare Logic\<close>
 
 theory Hoare
-imports Main
+  imports Main
 begin
 
 subsection \<open>Abstract syntax and semantics\<close>
@@ -34,28 +34,24 @@
 type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
-where
-  "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
-| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
+  where
+    "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
+  | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
 
 primrec Sem :: "'a com \<Rightarrow> 'a sem"
-where
-  "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
-| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
-    (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
-| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
+  where
+    "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
+  | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+  | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
+  | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
 
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-    ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
   where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
 
-lemma ValidI [intro?]:
-    "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
+lemma ValidI [intro?]: "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
   by (simp add: Valid_def)
 
-lemma ValidD [dest?]:
-    "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
+lemma ValidD [dest?]: "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
   by (simp add: Valid_def)
 
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>Using Hoare Logic\<close>
 
 theory Hoare_Ex
-imports Hoare
+  imports Hoare
 begin
 
 subsection \<open>State spaces\<close>
@@ -276,11 +276,11 @@
 type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
 
 primrec timeit :: "'a time com \<Rightarrow> 'a time com"
-where
-  "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
-| "timeit (c1; c2) = (timeit c1; timeit c2)"
-| "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-| "timeit (While b iv c) = While b iv (timeit c)"
+  where
+    "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
+  | "timeit (c1; c2) = (timeit c1; timeit c2)"
+  | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+  | "timeit (While b iv c) = While b iv (timeit c)"
 
 record tvars = tstate +
   I :: nat
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
 
 theory Knaster_Tarski
-imports Main "~~/src/HOL/Library/Lattice_Syntax"
+  imports Main "~~/src/HOL/Library/Lattice_Syntax"
 begin
 
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>The Mutilated Checker Board Problem\<close>
 
 theory Mutilated_Checkerboard
-imports Main
+  imports Main
 begin
 
 text \<open>
@@ -16,11 +16,10 @@
 
 subsection \<open>Tilings\<close>
 
-inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
-  for A :: "'a set set"
-where
-  empty: "{} \<in> tiling A"
-| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
+inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
+  where
+    empty: "{} \<in> tiling A"
+  | Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
 
 
 text \<open>The union of two disjoint tilings is a tiling.\<close>
@@ -114,9 +113,9 @@
 subsection \<open>Dominoes\<close>
 
 inductive_set domino :: "(nat \<times> nat) set set"
-where
-  horiz: "{(i, j), (i, j + 1)} \<in> domino"
-| vertl: "{(i, j), (i + 1, j)} \<in> domino"
+  where
+    horiz: "{(i, j), (i, j + 1)} \<in> domino"
+  | vertl: "{(i, j), (i + 1, j)} \<in> domino"
 
 lemma dominoes_tile_row:
   "{i} \<times> below (2 * n) \<in> tiling domino"
@@ -242,10 +241,8 @@
 subsection \<open>Main theorem\<close>
 
 definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
-  where
-    "mutilated_board m n =
-      below (2 * (m + 1)) \<times> below (2 * (n + 1))
-        - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+  where "mutilated_board m n =
+    below (2 * (m + 1)) \<times> below (2 * (n + 1)) - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
 
 theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
 proof (unfold mutilated_board_def)
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Peirce.thy
--- a/src/HOL/Isar_Examples/Peirce.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Peirce's Law\<close>
 
 theory Peirce
-imports Main
+  imports Main
 begin
 
 text \<open>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>An old chestnut\<close>
 
 theory Puzzle
-imports Main
+  imports Main
 begin
 
 text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Schroeder_Bernstein.thy
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Schröder-Bernstein Theorem\<close>
 
 theory Schroeder_Bernstein
-imports Main
+  imports Main
 begin
 
 text \<open>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Structured_Statements.thy
--- a/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Structured statements within Isar proofs\<close>
 
 theory Structured_Statements
-imports Main
+  imports Main
 begin
 
 subsection \<open>Introduction steps\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Isar_Examples/Summation.thy
--- a/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Summing natural numbers\<close>
 
 theory Summation
-imports Main
+  imports Main
 begin
 
 text \<open>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Library/Simps_Case_Conv.thy
--- a/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -5,8 +5,10 @@
 theory Simps_Case_Conv
 imports Main
 keywords
-  "simps_of_case" :: thy_decl == "" and
-  "case_of_simps" :: thy_decl
+  "simps_of_case" "case_of_simps" :: thy_decl
+abbrevs
+  "simps_of_case" = ""
+  "case_of_simps" = ""
 begin
 
 ML_file "simps_case_conv.ML"
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Nonstandard_Analysis/HLim.thy
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,8 @@
 section\<open>Limits and Continuity (Nonstandard)\<close>
 
 theory HLim
-imports Star
+  imports Star
+  abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
 begin
 
 text\<open>Nonstandard Definitions\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/HOL/Nonstandard_Analysis/HSEQ.thy
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -11,7 +11,8 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-imports Limits NatStar
+  imports Limits NatStar
+  abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
 definition
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -330,7 +330,7 @@
   private val caret_indicator = '\u0007'
   private val antiquote = "@{"
 
-  private val default_abbrs =
+  private val default_abbrevs =
     List("@{" -> "@{\u0007}",
       "`" -> "\\<close>",
       "`" -> "\\<open>",
@@ -340,11 +340,11 @@
       "\"" -> "\\<open>\u0007\\<close>")
 
   private def default_frequency(name: String): Option[Int] =
-    default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
+    default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
 }
 
 final class Completion private(
-  protected val keywords: Map[String, Boolean] = Map.empty,
+  protected val keywords: Set[String] = Set.empty,
   protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
   protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
@@ -363,8 +363,7 @@
     if (this eq other) this
     else if (is_empty) other
     else {
-      val keywords1 =
-        (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
       val words_lex1 = words_lex ++ other.words_lex
       val words_map1 = words_map ++ other.words_map
       val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
@@ -376,48 +375,52 @@
   /* keywords */
 
   private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
-  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
+  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
   private def is_keyword_template(name: String, template: Boolean): Boolean =
-    is_keyword(name) && keywords(name) == template
+    is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
 
-  def + (keyword: String, template: String): Completion =
-    new Completion(
-      keywords + (keyword -> (keyword != template)),
-      words_lex + keyword,
-      words_map + (keyword -> template),
-      abbrevs_lex,
-      abbrevs_map)
-
-  def + (keyword: String): Completion = this + (keyword, keyword)
+  def add_keyword(keyword: String): Completion =
+    new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
 
 
-  /* load symbols and abbrevs */
+  /* symbols and abbrevs */
 
-  private def load(): Completion =
+  def add_symbols(): Completion =
   {
-    val abbrevs = Completion.load_abbrevs()
-
     val words =
       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
-      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
-      (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
-
-    val non_word_abbrs =
-      (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
-        yield (abbr, text)).toList
-
-    val abbrs =
-      for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
-        yield (abbr.reverse, (abbr, text))
+      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
 
     new Completion(
       keywords,
       words_lex ++ words.map(_._1),
       words_map ++ words,
-      abbrevs_lex ++ abbrs.map(_._1),
-      abbrevs_map ++ abbrs)
+      abbrevs_lex,
+      abbrevs_map)
   }
 
+  def add_abbrevs(abbrevs: List[(String, String)]): Completion =
+    if (abbrevs.isEmpty) this
+    else {
+      val words =
+        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
+          yield (abbr, text)
+      val abbrs =
+        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
+          yield (abbr.reverse, (abbr, text))
+      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
+
+      new Completion(
+        keywords,
+        words_lex ++ words.map(_._1) -- remove,
+        words_map ++ words -- remove,
+        abbrevs_lex ++ abbrs.map(_._1) -- remove,
+        abbrevs_map ++ abbrs -- remove)
+    }
+
+  private def load(): Completion =
+    add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
+
 
   /* complete */
 
@@ -444,7 +447,7 @@
             case (abbr, _) :: _ =>
               val ok =
                 if (abbr == Completion.antiquote) language_context.antiquotes
-                else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr)
+                else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
               if (ok) Some((abbr, abbrevs))
               else None
           }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/General/multi_map.scala
--- a/src/Pure/General/multi_map.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/multi_map.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -8,6 +8,7 @@
 package isabelle
 
 
+import scala.collection.GenTraversableOnce
 import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
 
 
@@ -75,6 +76,9 @@
 
   def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
 
+  override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
+    (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
+
   def - (a: A): Multi_Map[A, B] =
     if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
 }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/scan.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -8,7 +8,7 @@
 
 
 import scala.annotation.tailrec
-import scala.collection.{IndexedSeq, TraversableOnce}
+import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
@@ -393,6 +393,11 @@
       else if (is_empty) other
       else this ++ other.raw_iterator
 
+    def -- (remove: Traversable[String]): Lexicon =
+      if (remove.exists(contains(_)))
+        Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
+      else this
+
 
     /* scan */
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -163,7 +163,7 @@
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
       (this /: header) {
-        case (keywords, (name, ((kind, exts), _), _)) =>
+        case (keywords, (name, ((kind, exts), _))) =>
           if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
           else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
       }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -76,7 +76,7 @@
   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
   val completion: Completion = Completion.empty,
   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
-  val has_tokens: Boolean = true) extends Prover.Syntax
+  val has_tokens: Boolean = true)
 {
   /** syntax content **/
 
@@ -85,30 +85,41 @@
 
   /* add keywords */
 
-  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
-    : Outer_Syntax =
+  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
   {
     val keywords1 = keywords + (name, kind, tags)
     val completion1 =
-      if (replace == Some("")) completion
-      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
-        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
-      else completion + (name, replace getOrElse name)
+      completion.add_keyword(name).add_abbrevs(
+        if (Keyword.theory_block.contains(kind))
+          List((name, name + "\nbegin\n\u0007\nend"), (name, name))
+        else List((name, name)))
     new Outer_Syntax(keywords1, completion1, language_context, true)
   }
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
-      case (syntax, (name, ((kind, tags), _), replace)) =>
-        syntax +
-          (Symbol.decode(name), kind, tags, replace) +
-          (Symbol.encode(name), kind, tags, replace)
+      case (syntax, (name, ((kind, tags), _))) =>
+        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+    }
+
+  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
+    if (abbrevs.isEmpty) this
+    else {
+      val completion1 =
+        completion.add_abbrevs(
+          (for ((a, b) <- abbrevs) yield {
+            val a1 = Symbol.decode(a)
+            val a2 = Symbol.encode(a)
+            val b1 = Symbol.decode(b)
+            List((a1, b1), (a2, b1))
+          }).flatten)
+      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
     }
 
 
   /* merge */
 
-  def ++ (other: Prover.Syntax): Prover.Syntax =
+  def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
     else {
       val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -326,7 +326,7 @@
     }
     else None
 
-  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+  def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
     syntax.load_command(span.name) match {
       case Some(exts) =>
         find_file(clean_tokens(span.content)) match {
@@ -340,7 +340,7 @@
 
   def blobs_info(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -83,6 +83,7 @@
     sealed case class Header(
       imports: List[(Name, Position.T)] = Nil,
       keywords: Thy_Header.Keywords = Nil,
+      abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
@@ -244,7 +245,7 @@
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.no_header,
-    val syntax: Option[Prover.Syntax] = None,
+    val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
@@ -268,7 +269,7 @@
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
-    def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
+    def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
       new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
 
     def update_perspective(
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -374,13 +374,12 @@
               val master_dir = File.standard_url(name.master_dir)
               val theory = Long_Name.base_name(name.theory)
               val imports = header.imports.map({ case (a, _) => a.node })
-              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
                 pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
                   pair(list(pair(Encode.string,
                     pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
                   list(Encode.string)))))(
-                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -13,18 +13,6 @@
 
 object Prover
 {
-  /* syntax */
-
-  trait Syntax
-  {
-    def ++ (other: Syntax): Syntax
-    def add_keywords(keywords: Thy_Header.Keywords): Syntax
-    def parse_spans(input: CharSequence): List[Command_Span.Span]
-    def load_command(name: String): Option[List[String]]
-    def load_commands_in(text: String): Boolean
-  }
-
-
   /* underlying system process */
 
   trait System_Process
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -23,7 +23,7 @@
 class Resources(
   val loaded_theories: Set[String],
   val known_theories: Map[String, Document.Node.Name],
-  val base_syntax: Prover.Syntax)
+  val base_syntax: Outer_Syntax)
 {
   /* document node names */
 
@@ -55,7 +55,7 @@
 
   /* theory files */
 
-  def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
+  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
       val spans = syntax.parse_spans(text)
       spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
@@ -103,7 +103,7 @@
 
         val imports =
           header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
-        Document.Node.Header(imports, header.keywords)
+        Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -237,7 +237,7 @@
   private val global_state = Synchronized(Document.State.init)
   def current_state(): Document.State = global_state.value
 
-  def recent_syntax(name: Document.Node.Name): Prover.Syntax =
+  def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.base_syntax
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,7 @@
 
 theory Pure
 keywords
-    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
+    "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
     "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
   and "private" "qualified" :: before_command
@@ -14,7 +14,7 @@
     "obtains" "shows" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
-  and "default_sort" :: thy_decl == ""
+  and "default_sort" :: thy_decl
   and "typedecl" "type_synonym" "nonterminal" "judgment"
     "consts" "syntax" "no_syntax" "translations" "no_translations"
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
@@ -25,7 +25,7 @@
   and "SML_import" "SML_export" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
-  and "simproc_setup" :: thy_decl % "ML" == ""
+  and "simproc_setup" :: thy_decl % "ML"
   and "setup" "local_setup" "attribute_setup" "method_setup"
     "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
@@ -47,9 +47,9 @@
   and "schematic_goal" :: thy_goal
   and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
-  and "hence" :: prf_goal % "proof" == "then have"
+  and "hence" :: prf_goal % "proof"
   and "show" :: prf_asm_goal % "proof"
-  and "thus" :: prf_asm_goal % "proof" == "then show"
+  and "thus" :: prf_asm_goal % "proof"
   and "then" "from" "with" :: prf_chain % "proof"
   and "note" :: prf_decl % "proof"
   and "supply" :: prf_script % "proof"
@@ -68,7 +68,7 @@
   and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
-  and "apply_end" :: prf_script % "proof" == ""
+  and "apply_end" :: prf_script % "proof"
   and "subgoal" :: prf_script_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
@@ -86,11 +86,19 @@
   and "display_drafts" "print_state" :: diag
   and "welcome" :: diag
   and "end" :: thy_end % "theory"
-  and "realizers" :: thy_decl == ""
-  and "realizability" :: thy_decl == ""
+  and "realizers" :: thy_decl
+  and "realizability" :: thy_decl
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
+abbrevs
+  "default_sort" = ""
+  "simproc_setup" = ""
+  "hence" = "then have"
+  "thus" = "then show"
+  "apply_end" = ""
+  "realizers" = ""
+  "realizability" = ""
 begin
 
 section \<open>Isar commands\<close>
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Aug 02 18:58:49 2016 +0200
@@ -58,6 +58,7 @@
 val theoryN = "theory";
 val importsN = "imports";
 val keywordsN = "keywords";
+val abbrevsN = "abbrevs";
 val beginN = "begin";
 
 val bootstrap_keywords =
@@ -68,11 +69,12 @@
      ((")", @{here}), Keyword.no_spec),
      ((",", @{here}), Keyword.no_spec),
      (("::", @{here}), Keyword.no_spec),
-     (("==", @{here}), Keyword.no_spec),
+     (("=", @{here}), Keyword.no_spec),
      (("and", @{here}), Keyword.no_spec),
      ((beginN, @{here}), Keyword.quasi_command_spec),
      ((importsN, @{here}), Keyword.quasi_command_spec),
      ((keywordsN, @{here}), Keyword.quasi_command_spec),
+     ((abbrevsN, @{here}), Keyword.quasi_command_spec),
      ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
      ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
      ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
@@ -128,14 +130,12 @@
   Parse.group (fn () => "outer syntax keyword specification")
     (Parse.name -- opt_files -- Parse.tags);
 
-val keyword_compl =
-  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
-
 val keyword_decl =
   Scan.repeat1 (Parse.position Parse.string) --
-  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
-  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
-  >> (fn ((names, spec), _) => map (rpair spec) names);
+  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
+  >> (fn (names, spec) => map (rpair spec) names);
+
+val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
 
 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
 
@@ -145,7 +145,8 @@
   Parse.position Parse.theory_name :|-- (fn (name, pos) =>
     imports name --
     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
-    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
+    (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
+    >> (fn (imports, keywords) => make (name, pos) imports keywords));
 
 end;
 
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -17,7 +17,8 @@
 {
   /* bootstrap keywords */
 
-  type Keywords = List[(String, Keyword.Spec, Option[String])]
+  type Keywords = List[(String, Keyword.Spec)]
+  type Abbrevs = List[(String, String)]
 
   val CHAPTER = "chapter"
   val SECTION = "section"
@@ -32,32 +33,34 @@
   val THEORY = "theory"
   val IMPORTS = "imports"
   val KEYWORDS = "keywords"
+  val ABBREVS = "abbrevs"
   val AND = "and"
   val BEGIN = "begin"
 
   private val bootstrap_header: Keywords =
     List(
-      ("%", Keyword.no_spec, None),
-      ("(", Keyword.no_spec, None),
-      (")", Keyword.no_spec, None),
-      (",", Keyword.no_spec, None),
-      ("::", Keyword.no_spec, None),
-      ("==", Keyword.no_spec, None),
-      (AND, Keyword.no_spec, None),
-      (BEGIN, Keyword.quasi_command_spec, None),
-      (IMPORTS, Keyword.quasi_command_spec, None),
-      (KEYWORDS, Keyword.quasi_command_spec, None),
-      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
-      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
-      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
-      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
-      ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
+      ("%", Keyword.no_spec),
+      ("(", Keyword.no_spec),
+      (")", Keyword.no_spec),
+      (",", Keyword.no_spec),
+      ("::", Keyword.no_spec),
+      ("=", Keyword.no_spec),
+      (AND, Keyword.no_spec),
+      (BEGIN, Keyword.quasi_command_spec),
+      (IMPORTS, Keyword.quasi_command_spec),
+      (KEYWORDS, Keyword.quasi_command_spec),
+      (ABBREVS, Keyword.quasi_command_spec),
+      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
+      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
+      ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
 
   private val bootstrap_keywords =
     Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -106,22 +109,26 @@
 
     val keyword_decl =
       rep1(string) ~
-      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
-      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
-      { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
+      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
+      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
 
     val keyword_decls =
       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
       { case xs ~ yss => (xs :: yss).flatten }
 
+    val abbrevs =
+      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
+
     val args =
       position(theory_name) ~
       (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt($$$(ABBREVS) ~! abbrevs) ^^
+        { case None => Nil case Some(_ ~ xs) => xs }) ~
       $$$(BEGIN) ^^
-      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
+      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
 
     val heading =
       (command(CHAPTER) |
@@ -171,13 +178,15 @@
 sealed case class Thy_Header(
   name: (String, Position.T),
   imports: List[(String, Position.T)],
-  keywords: Thy_Header.Keywords)
+  keywords: Thy_Header.Keywords,
+  abbrevs: Thy_Header.Abbrevs)
 {
   def decode_symbols: Thy_Header =
   {
     val f = Symbol.decode _
-    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
-      keywords.map({ case (a, ((x, y), z), c) =>
-        (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
+    Thy_Header((f(name._1), name._2),
+      imports.map({ case (a, b) => (f(a), b) }),
+      keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
+      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   }
 }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -38,24 +38,26 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
+    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Thy_Info.Dep],
     val keywords: Thy_Header.Keywords,
+    val abbrevs: Thy_Header.Abbrevs,
     val seen: Set[Document.Node.Name],
     val seen_names: Multi_Map[String, Document.Node.Name],
     val seen_positions: Multi_Map[String, Position.T])
   {
     def :: (dep: Thy_Info.Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
+      new Dependencies(
+        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
         seen, seen_names, seen_positions)
 
     def + (thy: (Document.Node.Name, Position.T)): Dependencies =
     {
       val (name, pos) = thy
-      new Dependencies(rev_deps, keywords,
+      new Dependencies(rev_deps, keywords, abbrevs,
         seen + name,
         seen_names + (name.theory -> name),
         seen_positions + (name.theory -> pos))
@@ -80,7 +82,8 @@
       header_errors ::: import_errors
     }
 
-    lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
+    lazy val syntax: Outer_Syntax =
+      resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
     def loaded_theories: Set[String] =
       (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
diff -r a4acecf4dc21 -r 71ee1b8067cc src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 18:58:49 2016 +0200
@@ -84,6 +84,7 @@
           val node1 = node.update_header(header)
           if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
               node.header.keywords != node1.header.keywords ||
+              node.header.abbrevs != node1.header.abbrevs ||
               node.header.errors != node1.header.errors) syntax_changed0 += name
           nodes += (name -> node1)
           doc_edits += (name -> Document.Node.Deps(header))
@@ -100,7 +101,8 @@
         else {
           val header = node.header
           val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
-          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
+          Some((resources.base_syntax /: imports_syntax)(_ ++ _)
+            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
         }
       nodes += (name -> node.update_syntax(syntax))
     }
@@ -156,7 +158,7 @@
 
   private def reparse_spans(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
@@ -202,7 +204,7 @@
 
   private def text_edit(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,