--- 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
-
--- 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"
--- 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"
--- 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!"
--- 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)"
--- 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"
--- 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 *}
--- 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"
--- 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
--- 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
--- 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
--- 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: