# HG changeset patch
# User wenzelm
# Date 1415709613 -3600
# Node ID cbc2ac19d783ed50e6a48ebd37514f3edcd04ff2
# Parent  2a683fb686fd01107a6fa9c7deb22320f14a1d4a
simplifie sessions;

diff -r 2a683fb686fd -r cbc2ac19d783 src/CCL/ROOT
--- a/src/CCL/ROOT	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CCL/ROOT	Tue Nov 11 13:40:13 2014 +0100
@@ -11,15 +11,13 @@
     evaluation to weak head-normal form.
   *}
   options [document = false]
-  theories Wfd Fix
+  theories
+    Wfd
+    Fix
 
-session "CCL-ex" in ex = CCL +
-  description {*
-    Author:     Martin Coen, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    (* Examples for Classical Computational Logic *)
+    "ex/Nat"
+    "ex/List"
+    "ex/Stream"
+    "ex/Flag"
 
-    Examples for Classical Computational Logic.
-  *}
-  options [document = false]
-  theories Nat List Stream Flag
-
diff -r 2a683fb686fd -r cbc2ac19d783 src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CCL/ex/Nat.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -6,7 +6,7 @@
 section {* Programs defined over the natural numbers *}
 
 theory Nat
-imports Wfd
+imports "../Wfd"
 begin
 
 definition not :: "i=>i"
diff -r 2a683fb686fd -r cbc2ac19d783 src/CTT/ROOT
--- a/src/CTT/ROOT	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CTT/ROOT	Tue Nov 11 13:40:13 2014 +0100
@@ -17,14 +17,11 @@
     1991)
   *}
   options [document = false]
-  theories Main
+  theories
+    Main
 
-session "CTT-ex" in ex = CTT +
-  description {*
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-    Examples for Constructive Type Theory.
-  *}
-  options [document = false]
-  theories Typechecking Elimination Equality Synthesis
+    (* Examples for Constructive Type Theory *)
+    "ex/Typechecking"
+    "ex/Elimination"
+    "ex/Equality"
+    "ex/Synthesis"
diff -r 2a683fb686fd -r cbc2ac19d783 src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CTT/ex/Elimination.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -9,7 +9,7 @@
 section "Examples with elimination rules"
 
 theory Elimination
-imports CTT
+imports "../CTT"
 begin
 
 text "This finds the functions fst and snd!"
diff -r 2a683fb686fd -r cbc2ac19d783 src/CTT/ex/Equality.thy
--- a/src/CTT/ex/Equality.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CTT/ex/Equality.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -6,7 +6,7 @@
 section "Equality reasoning by rewriting"
 
 theory Equality
-imports CTT
+imports "../CTT"
 begin
 
 lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
diff -r 2a683fb686fd -r cbc2ac19d783 src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CTT/ex/Synthesis.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -6,7 +6,7 @@
 section "Synthesis examples, using a crude form of narrowing"
 
 theory Synthesis
-imports Arith
+imports "../Arith"
 begin
 
 text "discovery of predecessor function"
diff -r 2a683fb686fd -r cbc2ac19d783 src/CTT/ex/Typechecking.thy
--- a/src/CTT/ex/Typechecking.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -6,7 +6,7 @@
 section "Easy examples: type checking and type deduction"
 
 theory Typechecking
-imports CTT
+imports "../CTT"
 begin
 
 subsection {* Single-step proofs: verifying that a type is well-formed *}
diff -r 2a683fb686fd -r cbc2ac19d783 src/LCF/ROOT
--- a/src/LCF/ROOT	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ROOT	Tue Nov 11 13:40:13 2014 +0100
@@ -11,19 +11,12 @@
     Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
   *}
   options [document = false]
-  theories LCF
-
-session "LCF-ex" in ex = LCF +
-  description {*
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
+  theories
+    LCF
 
-    Some examples from Lawrence Paulson's book Logic and Computation.
-  *}
-  options [document = false]
-  theories
-    Ex1
-    Ex2
-    Ex3
-    Ex4
+    (* Some examples from Lawrence Paulson's book Logic and Computation *)
+    "ex/Ex1"
+    "ex/Ex2"
+    "ex/Ex3"
+    "ex/Ex4"
 
diff -r 2a683fb686fd -r cbc2ac19d783 src/LCF/ex/Ex1.thy
--- a/src/LCF/ex/Ex1.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ex/Ex1.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -1,7 +1,7 @@
 section {*  Section 10.4 *}
 
 theory Ex1
-imports LCF
+imports "../LCF"
 begin
 
 axiomatization
diff -r 2a683fb686fd -r cbc2ac19d783 src/LCF/ex/Ex2.thy
--- a/src/LCF/ex/Ex2.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ex/Ex2.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -1,7 +1,7 @@
 section {* Example 3.8 *}
 
 theory Ex2
-imports LCF
+imports "../LCF"
 begin
 
 axiomatization
diff -r 2a683fb686fd -r cbc2ac19d783 src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ex/Ex3.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -1,7 +1,7 @@
 section {* Addition with fixpoint of successor *}
 
 theory Ex3
-imports LCF
+imports "../LCF"
 begin
 
 axiomatization
diff -r 2a683fb686fd -r cbc2ac19d783 src/LCF/ex/Ex4.thy
--- a/src/LCF/ex/Ex4.thy	Tue Nov 11 11:47:53 2014 +0100
+++ b/src/LCF/ex/Ex4.thy	Tue Nov 11 13:40:13 2014 +0100
@@ -2,7 +2,7 @@
 section {* Prefixpoints *}
 
 theory Ex4
-imports LCF
+imports "../LCF"
 begin
 
 lemma example: