1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/ROOT	Tue Jul 24 14:07:44 2012 +0200
     1.3 @@ -0,0 +1,21 @@
     1.4 +session CCL! in "." = Pure +
     1.5 +  description {*
     1.6 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +    Classical Computational Logic based on First-Order Logic.
    1.10 +
    1.11 +    A computational logic for an untyped functional language with
    1.12 +    evaluation to weak head-normal form.
    1.13 +  *}
    1.14 +  theories Wfd Fix
    1.15 +
    1.16 +session ex = CCL +
    1.17 +  description {*
    1.18 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    1.19 +    Copyright   1993  University of Cambridge
    1.20 +
    1.21 +    Examples for Classical Computational Logic.
    1.22 +  *}
    1.23 +  theories Nat List Stream Flag
    1.24 +

     2.1 --- a/src/CCL/Set.thy	Tue Jul 24 13:22:06 2012 +0200
     2.2 +++ b/src/CCL/Set.thy	Tue Jul 24 14:07:44 2012 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  header {* Extending FOL by a modified version of HOL set theory *}
     2.5  
     2.6  theory Set
     2.7 -imports FOL
     2.8 +imports "~~/src/FOL/FOL"
     2.9  begin
    2.10  
    2.11  declare [[eta_contract]]

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/CTT/ROOT	Tue Jul 24 14:07:44 2012 +0200
     3.3 @@ -0,0 +1,15 @@
     3.4 +session CTT! in "." = Pure +
     3.5 +  description {*
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +  *}
     3.9 +  theories Main
    3.10 +
    3.11 +session ex = CTT +
    3.12 +  description {*
    3.13 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.14 +    Copyright   1991  University of Cambridge
    3.15 +
    3.16 +    Examples for Constructive Type Theory.
    3.17 +  *}
    3.18 +  theories Typechecking Elimination Equality Synthesis

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Cube/ROOT	Tue Jul 24 14:07:44 2012 +0200
     4.3 @@ -0,0 +1,9 @@
     4.4 +session Cube! in "." = Pure +
     4.5 +  description {*
     4.6 +    Author:     Tobias Nipkow
     4.7 +    Copyright   1992  University of Cambridge
     4.8 +
     4.9 +    The Lambda-Cube a la Barendregt.
    4.10 +  *}
    4.11 +  theories Example
    4.12 +

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/FOLP/ROOT	Tue Jul 24 14:07:44 2012 +0200
     5.3 @@ -0,0 +1,30 @@
     5.4 +session FOLP! in "." = Pure +
     5.5 +  description {*
     5.6 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     5.7 +    Copyright   1993  University of Cambridge
     5.8 +
     5.9 +    Modifed version of FOL that contains proof terms.
    5.10 +
    5.11 +    Presence of unknown proof term means that matching does not behave as expected.
    5.12 +  *}
    5.13 +  theories FOLP
    5.14 +
    5.15 +session ex = FOLP +
    5.16 +  description {*
    5.17 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.18 +    Copyright   1992  University of Cambridge
    5.19 +
    5.20 +    Examples for First-Order Logic.
    5.21 +  *}
    5.22 +  theories
    5.23 +    Intro
    5.24 +    Nat
    5.25 +    Foundation
    5.26 +    If
    5.27 +    Intuitionistic
    5.28 +    Classical
    5.29 +    Propositional_Int
    5.30 +    Quantifiers_Int
    5.31 +    Propositional_Cla
    5.32 +    Quantifiers_Cla
    5.33 +

     6.1 --- a/src/LCF/LCF.thy	Tue Jul 24 13:22:06 2012 +0200
     6.2 +++ b/src/LCF/LCF.thy	Tue Jul 24 14:07:44 2012 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* LCF on top of First-Order Logic *}
     6.5  
     6.6  theory LCF
     6.7 -imports FOL
     6.8 +imports "~~/src/FOL/FOL"
     6.9  begin
    6.10  
    6.11  text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/LCF/ROOT	Tue Jul 24 14:07:44 2012 +0200
     7.3 @@ -0,0 +1,16 @@
     7.4 +session LCF! in "." = Pure +
     7.5 +  description {*
     7.6 +    Author:     Tobias Nipkow
     7.7 +    Copyright   1992  University of Cambridge
     7.8 +  *}
     7.9 +  theories LCF
    7.10 +
    7.11 +session ex = LCF +
    7.12 +  description {*
    7.13 +    Author:     Tobias Nipkow
    7.14 +    Copyright   1991  University of Cambridge
    7.15 +
    7.16 +    Some examples from Lawrence Paulson's book Logic and Computation.
    7.17 +  *}
    7.18 +  theories Ex1 Ex2 Ex3 Ex4
    7.19 +

     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Sequents/ROOT	Tue Jul 24 14:07:44 2012 +0200
     8.3 @@ -0,0 +1,18 @@
     8.4 +session Sequents! in "." = Pure +
     8.5 +  description {*
     8.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1991  University of Cambridge
     8.8 +
     8.9 +    Classical Sequent Calculus based on Pure Isabelle.
    8.10 +  *}
    8.11 +  theories LK ILL ILL_predlog Washing Modal0 T S4 S43
    8.12 +
    8.13 +session LK = Sequents +
    8.14 +  description {*
    8.15 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    8.16 +    Copyright   1992  University of Cambridge
    8.17 +
    8.18 +    Examples for Classical Logic.
    8.19 +  *}
    8.20 +  theories Propositional Quantifiers Hard_Quantifiers Nat
    8.21 +