diff --git a/src/Pure/ROOT b/src/Pure/ROOT
--- a/src/Pure/ROOT
+++ b/src/Pure/ROOT
@@ -1,23 +1,31 @@
 chapter Pure
 
 session Pure =
   description "
     The Pure logical framework.
   "
   options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false]
   theories [export_theory]
     Pure (global)
   theories
     ML_Bootstrap (global)
     Sessions
 
 session "Pure-Examples" in Examples = Pure +
   description "
     Notable Examples for Isabelle/Pure.
   "
   theories
     First_Order_Logic
     Higher_Order_Logic
   document_files
     "root.bib"
     "root.tex"
+
+session "Pure-ex" in ex = Pure +
+  description "
+    Miscellaneous examples and experiments for Isabelle/Pure.
+  "
+  theories
+    Def
+    Def_Examples
diff --git a/src/Pure/ex/Def.thy b/src/Pure/ex/Def.thy
new file mode 100644
--- /dev/null
+++ b/src/Pure/ex/Def.thy
@@ -0,0 +1,113 @@
+(*  Title:      Pure/ex/Def.thy
+    Author:     Makarius
+
+Primitive constant definition, without fact definition;
+automatic expansion via Simplifier (simproc).
+*)
+
+theory Def
+  imports Pure
+  keywords "def" :: thy_defn
+begin
+
+ML \<open>
+signature DEF =
+sig
+  val get_def: Proof.context -> cterm -> thm option
+  val def: (binding * typ option * mixfix) option ->
+    (binding * typ option * mixfix) list -> term -> local_theory -> term * local_theory
+  val def_cmd: (binding * string option * mixfix) option ->
+    (binding * string option * mixfix) list -> string -> local_theory -> term * local_theory
+end;
+
+structure Def: DEF =
+struct
+
+(* context data *)
+
+type def = {lhs: term, mk_eq: morphism -> thm};
+
+val eq_def : def * def -> bool = op aconv o apply2 #lhs;
+
+fun transform_def phi ({lhs, mk_eq}: def) =
+  {lhs = Morphism.term phi lhs, mk_eq = Morphism.transform phi mk_eq};
+
+structure Data = Generic_Data
+(
+  type T = def Item_Net.T;
+  val empty : T = Item_Net.init eq_def (single o #lhs);
+  val extend = I;
+  val merge = Item_Net.merge;
+);
+
+fun declare_def lhs eq lthy =
+  let
+    val eq0 = Thm.trim_context eq;
+    val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0};
+  in
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+      (fn phi => (Data.map o Item_Net.update) (transform_def phi def))
+  end;
+
+fun get_def ctxt ct =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val data = Data.get (Context.Proof ctxt);
+    val t = Thm.term_of ct;
+    fun match_def {lhs, mk_eq} =
+      if Pattern.matches thy (lhs, t) then
+        let
+          val inst = Thm.match (Thm.cterm_of ctxt lhs, ct);
+          val eq =
+            Morphism.form mk_eq
+            |> Thm.transfer thy
+            |> Thm.instantiate inst;
+        in SOME eq end
+      else NONE;
+  in Item_Net.retrieve_matching data t |> get_first match_def end;
+
+
+(* simproc setup *)
+
+val _ =
+  (Theory.setup o Named_Target.theory_map)
+    (Simplifier.define_simproc \<^binding>\<open>expand_def\<close>
+      {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def});
+
+
+(* Isar command *)
+
+fun gen_def prep_spec raw_var raw_params raw_spec lthy =
+  let
+    val ((vars, xs, get_pos, spec), _) = lthy
+      |> prep_spec (the_list raw_var) raw_params [] raw_spec;
+    val (((x, _), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = false} spec;
+    val _ = Name.reject_internal (x, []);
+    val (b, mx) =
+      (case (vars, xs) of
+        ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn)
+      | ([(b, _, mx)], [y]) =>
+          if x = y then (b, mx)
+          else
+            error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+              Position.here (Binding.pos_of b)));
+    val ((lhs, (_, eq)), lthy') = lthy
+      |> Local_Theory.define_internal ((b, mx), (Binding.empty_atts, rhs));
+
+    (*sanity check for original specification*)
+    val _: thm = prove lthy' eq;
+  in (lhs, declare_def lhs eq lthy') end;
+
+val def = gen_def Specification.check_spec_open;
+val def_cmd = gen_def Specification.read_spec_open;
+
+val _ =
+  Outer_Syntax.local_theory \<^command_keyword>\<open>def\<close>
+    "primitive constant definition, without fact definition"
+    (Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
+      >> (fn ((decl, spec), params) => #2 o def_cmd decl params spec));
+
+end;
+\<close>
+
+end
diff --git a/src/Pure/ex/Def_Examples.thy b/src/Pure/ex/Def_Examples.thy
new file mode 100644
--- /dev/null
+++ b/src/Pure/ex/Def_Examples.thy
@@ -0,0 +1,43 @@
+(*  Title:      Pure/ex/Def_Examples.thy
+    Author:     Makarius
+
+Some examples for primitive definitions.
+*)
+
+theory Def_Examples
+  imports Def
+begin
+
+section \<open>Global definitions\<close>
+
+def "I x \<equiv> x"
+def "K x y \<equiv> x"
+def "S x y z \<equiv> (x z) (y z)"
+
+lemma "I (I x) \<equiv> x"
+  by simp
+
+lemma "K a x \<equiv> K a y"
+  by simp
+
+lemma "S K K \<equiv> I"
+  by simp
+
+
+section \<open>Locale definitions\<close>
+
+locale const =
+  fixes a :: 'a
+begin
+
+def "fun b \<equiv> a"
+
+lemma "fun x \<equiv> fun y"
+  by simp
+
+end
+
+lemma "const.fun a x \<equiv> const.fun a y"
+  by simp
+
+end