From 8606f8bfd3f85aaea52a9a6374adb2e33b6a2a0a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 30 Jun 2002 17:41:31 +0000 Subject: New files. --- etc/isar/Persistent.thy | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 etc/isar/Persistent.thy (limited to 'etc/isar') diff --git a/etc/isar/Persistent.thy b/etc/isar/Persistent.thy new file mode 100644 index 00000000..a4ade1f9 --- /dev/null +++ b/etc/isar/Persistent.thy @@ -0,0 +1,40 @@ +(* + +We now support persistent Isabelle sessions with Proof General, preserving +the state of loaded theories (before I used to have a few explicit +``bombs'' to prevent this). When saying ``Exit Isabelle/Isar'' the image +is committed back. It's not possible to go continue partially processed +theory buffer, but users could expect to have a fully processed theory +stored properly. The latter requires scripting to be disabled first, in +order to inform the process to store the finished theory. + +To spare users to think about this, the ``Exit Isabelle/Isar'' +operation disables scripting automatically. + +Produce a writable Isabelle session like this: + + isabelle -q HOL Foo + +Now start PG and start a process with the Foo logic image. + +Tests: + + Process this file, exit, start. + Unprocess, exit, start. [FAILS] + +*) + + +theory Persistent = Main: + +theorem and_comms: "A & B --> B & A" +proof + assume "A & B" + then show "B & A" + proof + assume B and A + then show ?thesis .. + qed +qed + +end -- cgit v1.2.3