# HG changeset patch
# User wenzelm
# Date 964954251 -7200
# Node ID 4362bf779182ae14e288d0ab4326dde454d24152
# Parent  3ac87f80186d5b233259eddffd146ccedd62064d
ObtainFun (generalized existence reasoning);

diff -r 3ac87f80186d -r 4362bf779182 src/Pure/Isar/README
--- a/src/Pure/Isar/README	Sun Jul 30 12:50:33 2000 +0200
+++ b/src/Pure/Isar/README	Sun Jul 30 12:50:51 2000 +0200
@@ -11,6 +11,7 @@
 
   LocalDefs	(local definitions)
   Calculation	(calculational proofs)
+  ObtainFun     (generalized existence reasoning)
 
   Toplevel	(the Isabelle/Isar toplevel)
   IsarThy	(Isar derived theory operations)