--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ROOT Tue Jul 17 22:34:29 2012 +0200
@@ -0,0 +1,27 @@
+session FOL in "." = Pure +
+ name FOL
+ description "First-Order Logic with Natural Deduction"
+ options [proofs = 2]
+ theories FOL
+ files "document/root.tex"
+
+session ex = FOL +
+ theories
+ First_Order_Logic
+ Natural_Numbers
+ Intro
+ Nat
+ Nat_Class
+ Foundation
+ Prolog
+ Intuitionistic
+ Propositional_Int
+ Quantifiers_Int
+ Classical
+ Propositional_Cla
+ Quantifiers_Cla
+ Miniscope
+ If
+ theories [document = false] "Locale_Test/Locale_Test"
+ files "document/root.tex"
+
--- a/src/Pure/System/build.scala Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Pure/System/build.scala Tue Jul 17 22:34:29 2012 +0200
@@ -56,5 +56,24 @@
rc
}
+
+
+ /* session information */
+
+ case class Session_Info(
+ val dir: Path,
+ val text: String)
+
+ val ROOT_NAME = "ROOT"
+
+ def find_sessions(): List[Session_Info] =
+ {
+ for {
+ dir <- Isabelle_System.components()
+ root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
+ if root.isFile
+ }
+ yield Session_Info(dir, Standard_System.read_file(root))
+ }
}
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jul 17 22:34:29 2012 +0200
@@ -230,7 +230,7 @@
perl -i -e 'while (<>) {
if (m/NAME="javacc"/) {
print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
- print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
+ print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
elsif (m/NAME="scheme"/) {
print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
print; }' dist/modes/catalog
--- a/src/Tools/jEdit/src/modes/isabelle-session.xml Tue Jul 17 21:49:32 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-session.xml Tue Jul 17 22:34:29 2012 +0200
@@ -21,21 +21,22 @@
<BEGIN>{*</BEGIN>
<END>*}</END>
</SPAN>
- <SPAN TYPE="LITERAL1">
+ <SPAN TYPE="LITERAL2">
<BEGIN>`</BEGIN>
<END>`</END>
</SPAN>
- <SPAN TYPE="LITERAL3">
+ <SPAN TYPE="LITERAL1">
<BEGIN>"</BEGIN>
<END>"</END>
</SPAN>
<KEYWORDS>
<KEYWORD1>session</KEYWORD1>
- <KEYWORD2>parent</KEYWORD2>
- <KEYWORD2>imports</KEYWORD2>
- <KEYWORD2>uses</KEYWORD2>
+ <KEYWORD2>in</KEYWORD2>
+ <KEYWORD2>name</KEYWORD2>
+ <KEYWORD2>description</KEYWORD2>
+ <KEYWORD2>files</KEYWORD2>
<KEYWORD2>options</KEYWORD2>
- <KEYWORD2>dependencies</KEYWORD2>
+ <KEYWORD2>theories</KEYWORD2>
</KEYWORDS>
</RULES>
</MODE>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ROOT Tue Jul 17 22:34:29 2012 +0200
@@ -0,0 +1,148 @@
+session ZF in "." = FOL +
+ name ZF
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+ Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+
+ This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+ *}
+ options [document_graph]
+ theories Main Main_ZFC
+ files "document/root.tex"
+
+session AC = ZF +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+ Proofs of AC-equivalences, due to Krzysztof Grabczewski.
+ *}
+ options [document_graph]
+ theories WO6_WO1 WO1_WO7 AC7_AC9 WO1_AC AC15_WO6
+ WO2_AC16 AC16_WO4 AC17_AC1 AC18_AC19 DC
+ files "document/root.tex" "document/root.bib"
+
+session Coind = ZF +
+ description {*
+ Author: Jacob Frost, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+ Coind -- A Coinduction Example.
+
+ Based upon the article
+ Robin Milner and Mads Tofte,
+ Co-induction in Relational Semantics,
+ Theoretical Computer Science 87 (1991), pages 209-220.
+
+ Written up as
+ Jacob Frost, A Case Study of Co_induction in Isabelle
+ Report, Computer Lab, University of Cambridge (1995).
+ *}
+ theories ECR
+
+session Constructible = ZF +
+ description {* Inner Models, Absoluteness and Consistency Proofs. *}
+ options [document_graph]
+ theories DPow_absolute AC_in_L Rank_Separation
+ files "document/root.tex" "document/root.bib"
+
+session IMP = ZF +
+ description {*
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Copyright 1994 TUM
+
+ Formalization of the denotational and operational semantics of a
+ simple while-language, including an equivalence proof.
+
+ The whole development essentially formalizes/transcribes
+ chapters 2 and 5 of
+
+ Glynn Winskel. The Formal Semantics of Programming Languages.
+ MIT Press, 1993.
+ *}
+ theories Equiv
+ files "document/root.tex" "document/root.bib"
+
+session Induct = ZF +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+ Inductive definitions.
+ *}
+ theories
+ (** Datatypes **)
+ Datatypes (*sample datatypes*)
+ Binary_Trees (*binary trees*)
+ Term (*recursion over the list functor*)
+ Ntree (*variable-branching trees; function demo*)
+ Tree_Forest (*mutual recursion*)
+ Brouwer (*Infinite-branching trees*)
+ Mutil (*mutilated chess board*)
+
+ (*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for
+ finite sets*)
+ Multiset
+ Rmap (*mapping a relation over a list*)
+ PropLog (*completeness of propositional logic*)
+
+ (*two Coq examples by Christine Paulin-Mohring*)
+ ListN
+ Acc
+
+ Comb (*Combinatory Logic example*)
+ Primrec (*Primitive recursive functions*)
+ files "document/root.tex"
+
+session Resid = ZF +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+ Residuals -- a proof of the Church-Rosser Theorem for the
+ untyped lambda-calculus.
+
+ By Ole Rasmussen, following the Coq proof given in
+
+ Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
+ J. Functional Programming 4(3) 1994, 371-394.
+ *}
+ theories Confluence
+
+session UNITY = ZF +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+ ZF/UNITY proofs.
+ *}
+ theories
+ (*Simple examples: no composition*)
+ Mutex
+
+ (*Basic meta-theory*)
+ Guar
+
+ (*Prefix relation; the Allocator example*)
+ Distributor Merge ClientImpl AllocImpl
+
+session ex = ZF +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+ Miscellaneous examples for Zermelo-Fraenkel Set Theory.
+ *}
+ theories
+ misc
+ Ring (*abstract algebra*)
+ Commutation (*abstract Church-Rosser theory*)
+ Primes (*GCD theory*)
+ NatSum (*Summing integers, squares, cubes, etc.*)
+ Ramsey (*Simple form of Ramsey's theorem*)
+ Limit (*Inverse limit construction of domains*)
+ BinEx (*Binary integer arithmetic*)
+ LList CoUnit (*CoDatatypes*)
+