From 51c70ccb7627a871fe7f73632b57a4ca68575f4d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 26 Jul 2006 13:42:35 +0000
Subject: Change to new Isabelle syntax

---
 etc/isar/multiple/A.thy | 3 ++-
 etc/isar/multiple/B.thy | 6 +++---
 etc/isar/multiple/C.thy | 5 +++--
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/etc/isar/multiple/A.thy b/etc/isar/multiple/A.thy
index 7ad1ddf6..5c11b4fe 100644
--- a/etc/isar/multiple/A.thy
+++ b/etc/isar/multiple/A.thy
@@ -1,5 +1,6 @@
 
-theory A = Pure:;
+theory A imports Pure 
+begin
 
 consts foo :: 'a;
 consts bar :: 'a;
diff --git a/etc/isar/multiple/B.thy b/etc/isar/multiple/B.thy
index 2828c655..efebff83 100644
--- a/etc/isar/multiple/B.thy
+++ b/etc/isar/multiple/B.thy
@@ -1,4 +1,4 @@
+theory B imports Pure
+begin
 
-theory B = Pure:;
-
-end;
+end
diff --git a/etc/isar/multiple/C.thy b/etc/isar/multiple/C.thy
index d295f55a..079a1f78 100644
--- a/etc/isar/multiple/C.thy
+++ b/etc/isar/multiple/C.thy
@@ -1,5 +1,6 @@
 (* -*- isar -*- *)
 
-theory C = A + B:;
+theory C imports A B
+begin
 
-end;
+end
-- 
cgit v1.2.3