# HG changeset patch
# User wenzelm
# Date 1458205238 -3600
# Node ID dfd6fe970503c470fc39d3e671d7d1e93f24859b
# Parent  47635cd9a996a79314ce24e5ebf0696a03ed57ae
obsolete;

diff -r 47635cd9a996 -r dfd6fe970503 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 09:59:37 2016 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 10:00:38 2016 +0100
@@ -581,17 +581,6 @@
   Simplifier, which is also known as ``simpset'' internally; the ``\<open>!\<close>''
   option indicates extra verbosity.
 
-  For historical reasons, simpsets may occur independently from the current
-  context, but are conceptually dependent on it. When the Simplifier is
-  invoked via one of its main entry points in the Isar source language (as
-  proof method \secref{sec:simp-meth} or rule attribute
-  \secref{sec:simp-meth}), its simpset is derived from the current proof
-  context, and carries a back-reference to that for other tools that might get
-  invoked internally (e.g.\ simplification procedures \secref{sec:simproc}). A
-  mismatch of the context of the simpset and the context of the problem being
-  simplified may lead to unexpected results.
-
-
   The implicit simpset of the theory context is propagated monotonically
   through the theory hierarchy: forming a new theory, the union of the
   simpsets of its imports are taken as starting point. Also note that