ObtainFun (generalized existence reasoning);
authorwenzelm
Sun, 30 Jul 2000 12:50:51 +0200
changeset 9463 4362bf779182
parent 9462 3ac87f80186d
child 9464 e290583864e4
ObtainFun (generalized existence reasoning);
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)