--- a/etc/options Tue Jul 24 12:36:59 2012 +0200
+++ b/etc/options Tue Jul 24 21:48:41 2012 +0200
@@ -1,24 +1,30 @@
(* :mode=isabelle-options: *)
declare browser_info : bool = false
+declare browser_info_remote : string = ""
-declare document : bool = true
-declare document_format : string = pdf
-declare document_variants : string = document
+declare document : string = ""
+declare document_variants : string = "outline=/proof,/ML"
declare document_graph : bool = false
+declare document_dump : string = ""
+declare document_dump_only : bool = false
+declare no_document : bool = false
-declare threads_limit : int = 1
+declare threads : int = 0
declare threads_trace : int = 0
-declare parallel_proofs : int = 1
+declare parallel_proofs : int = 2
declare parallel_proofs_threshold : int = 100
declare print_mode : string = ""
-declare proofs : int = 0
+declare proofs : int = 1
declare quick_and_dirty : bool = false
-declare timing : bool = false
-declare verbose : bool = false
-
declare condition : string = ""
+declare show_question_marks : bool = true
+
+declare names_long : bool = false
+declare names_short : bool = false
+declare names_unique : bool = true
+
--- a/etc/settings Tue Jul 24 12:36:59 2012 +0200
+++ b/etc/settings Tue Jul 24 21:48:41 2012 +0200
@@ -67,11 +67,15 @@
###
-### Batch sessions (cf. isabelle usedir)
+### Batch sessions
###
+#cf. isabelle usedir
ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
+#cf. isabelle build
+ISABELLE_BUILD_OPTIONS=""
+
###
### Document preparation (cf. isabelle latex/document)
--- a/lib/Tools/build Tue Jul 24 12:36:59 2012 +0200
+++ b/lib/Tools/build Tue Jul 24 21:48:41 2012 +0200
@@ -9,6 +9,17 @@
PRG="$(basename "$0")"
+function show_settings()
+{
+ local PREFIX="$1"
+ echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
+ echo
+ echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
+ echo "${PREFIX}ML_HOME=\"$ML_HOME\""
+ echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
+ echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
+}
+
function usage()
{
echo
@@ -19,18 +30,14 @@
echo " -b build target images"
echo " -d DIR additional session directory with ROOT file"
echo " -j INT maximum number of jobs (default 1)"
- echo " -l list sessions only"
+ echo " -n no build -- test dependencies only"
echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
echo " -s system build mode: produce output in ISABELLE_HOME"
+ echo " -t inner session timing"
echo " -v verbose"
echo
echo " Build and manage Isabelle sessions, depending on implicit"
- echo " ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
- echo
- echo " ML_PLATFORM=\"$ML_PLATFORM\""
- echo " ML_HOME=\"$ML_HOME\""
- echo " ML_SYSTEM=\"$ML_SYSTEM\""
- echo " ML_OPTIONS=\"$ML_OPTIONS\""
+ show_settings " "
echo
exit 1
}
@@ -52,14 +59,15 @@
ALL_SESSIONS=false
BUILD_IMAGES=false
MAX_JOBS=1
-LIST_ONLY=false
+NO_BUILD=false
SYSTEM_MODE=false
+TIMING=false
VERBOSE=false
declare -a MORE_DIRS=()
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
-while getopts "abd:j:lo:sv" OPT
+while getopts "abd:j:no:stv" OPT
do
case "$OPT" in
a)
@@ -75,8 +83,8 @@
check_number "$OPTARG"
MAX_JOBS="$OPTARG"
;;
- l)
- LIST_ONLY="true"
+ n)
+ NO_BUILD="true"
;;
o)
BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
@@ -84,6 +92,9 @@
s)
SYSTEM_MODE="true"
;;
+ t)
+ TIMING="true"
+ ;;
v)
VERBOSE="true"
;;
@@ -100,6 +111,26 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
-exec "$ISABELLE_TOOL" java isabelle.Build \
- "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
- "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+if [ "$NO_BUILD" = false ]; then
+ echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
+
+ if [ "$VERBOSE" = true ]; then
+ show_settings ""
+ echo
+ fi
+ . "$ISABELLE_HOME/lib/scripts/timestart.bash"
+fi
+
+"$ISABELLE_TOOL" java isabelle.Build \
+ "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" \
+ "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+RC="$?"
+
+if [ "$NO_BUILD" = false ]; then
+ echo -n "Finished at "; date
+
+ . "$ISABELLE_HOME/lib/scripts/timestop.bash"
+ echo "$TIMES_REPORT"
+fi
+
+exit "$RC"
--- a/lib/scripts/getsettings Tue Jul 24 12:36:59 2012 +0200
+++ b/lib/scripts/getsettings Tue Jul 24 21:48:41 2012 +0200
@@ -51,6 +51,10 @@
#platform
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
+if [ -z "$ISABELLE_PLATFORM" ]; then
+ echo 1>&2 "Failed to determine hardware and operating system type!"
+ exit 2
+fi
#Isabelle distribution identifier -- filled in automatically!
ISABELLE_ID=""
--- a/lib/scripts/isabelle-platform Tue Jul 24 12:36:59 2012 +0200
+++ b/lib/scripts/isabelle-platform Tue Jul 24 21:48:41 2012 +0200
@@ -4,17 +4,17 @@
#
# NOTE: The ML system or JVM may have their own idea about the platform!
-ISABELLE_PLATFORM="unknown-platform"
+ISABELLE_PLATFORM32=""
ISABELLE_PLATFORM64=""
case $(uname -s) in
Linux)
case $(uname -m) in
i?86)
- ISABELLE_PLATFORM=x86-linux
+ ISABELLE_PLATFORM32=x86-linux
;;
x86_64)
- ISABELLE_PLATFORM=x86-linux
+ ISABELLE_PLATFORM32=x86-linux
ISABELLE_PLATFORM64=x86_64-linux
;;
esac
@@ -22,47 +22,32 @@
Darwin)
case $(uname -m) in
i?86)
- ISABELLE_PLATFORM=x86-darwin
+ ISABELLE_PLATFORM32=x86-darwin
if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then
ISABELLE_PLATFORM64=x86_64-darwin
fi
;;
x86_64)
- ISABELLE_PLATFORM=x86-darwin
+ ISABELLE_PLATFORM32=x86-darwin
ISABELLE_PLATFORM64=x86_64-darwin
;;
- Power* | power* | ppc)
- ISABELLE_PLATFORM=ppc-darwin
- ;;
esac
;;
CYGWIN_NT*)
case $(uname -m) in
i?86 | x86_64)
- ISABELLE_PLATFORM=x86-cygwin
- ;;
- esac
- ;;
- SunOS)
- case $(uname -r) in
- 5.*)
- case $(uname -p) in
- sparc)
- ISABELLE_PLATFORM=sparc-solaris
- ;;
- i?86 | x86_64)
- ISABELLE_PLATFORM=x86-solaris
- ;;
- esac
+ ISABELLE_PLATFORM32=x86-cygwin
;;
esac
;;
*BSD)
case $(uname -m) in
i?86 | x86_64)
- ISABELLE_PLATFORM=x86-linux
+ ISABELLE_PLATFORM32=x86-linux #cf. BSD Linux Binary Compatibility
;;
esac
;;
esac
+ISABELLE_PLATFORM="$ISABELLE_PLATFORM32"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,23 @@
+session CCL! in "." = Pure +
+ description {*
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+ Classical Computational Logic based on First-Order Logic.
+
+ A computational logic for an untyped functional language with
+ evaluation to weak head-normal form.
+ *}
+ options [document = false]
+ theories Wfd Fix
+
+session ex = CCL +
+ description {*
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+ Examples for Classical Computational Logic.
+ *}
+ options [document = false]
+ theories Nat List Stream Flag
+
--- a/src/CCL/Set.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/CCL/Set.thy Tue Jul 24 21:48:41 2012 +0200
@@ -1,7 +1,7 @@
header {* Extending FOL by a modified version of HOL set theory *}
theory Set
-imports FOL
+imports "~~/src/FOL/FOL"
begin
declare [[eta_contract]]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,17 @@
+session CTT! in "." = Pure +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+ *}
+ options [document = false]
+ theories Main
+
+session 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,10 @@
+session Cube! in "." = Pure +
+ description {*
+ Author: Tobias Nipkow
+ Copyright 1992 University of Cambridge
+
+ The Lambda-Cube a la Barendregt.
+ *}
+ options [document = false]
+ theories Example
+
--- a/src/FOL/ROOT Tue Jul 24 12:36:59 2012 +0200
+++ b/src/FOL/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -1,4 +1,4 @@
-session FOL! (10) in "." = Pure +
+session FOL! in "." = Pure +
description "First-Order Logic with Natural Deduction"
options [proofs = 2]
theories FOL
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,32 @@
+session FOLP! in "." = Pure +
+ description {*
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+ Modifed version of FOL that contains proof terms.
+
+ Presence of unknown proof term means that matching does not behave as expected.
+ *}
+ options [document = false]
+ theories FOLP
+
+session ex = FOLP +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+ Examples for First-Order Logic.
+ *}
+ options [document = false]
+ theories
+ Intro
+ Nat
+ Foundation
+ If
+ Intuitionistic
+ Classical
+ Propositional_Int
+ Quantifiers_Int
+ Propositional_Cla
+ Quantifiers_Cla
+
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Tue Jul 24 21:48:41 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Johannes Hoelzl <hoelzl@in.tum.de> 2009 *)
theory Approximation_Ex
-imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation"
+imports Complex_Main "../Approximation"
begin
text {*
--- a/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy Tue Jul 24 21:48:41 2012 +0200
@@ -3,7 +3,7 @@
header {* Some examples demonstrating the comm-ring method *}
theory Commutative_Ring_Ex
-imports Commutative_Ring
+imports "../Commutative_Ring"
begin
lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243"
--- a/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Tue Jul 24 21:48:41 2012 +0200
@@ -3,7 +3,7 @@
header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *}
theory Dense_Linear_Order_Ex
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports "../Dense_Linear_Order"
begin
lemma
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Tue Jul 24 21:48:41 2012 +0200
@@ -3,7 +3,7 @@
header "Denotational Abstract Interpretation"
theory Abs_Int_den0_fun
-imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
+imports "~~/src/HOL/ex/Interpretation_with_Defs" "../Big_Step"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Tue Jul 24 21:48:41 2012 +0200
@@ -5,7 +5,7 @@
theory Abs_Int0_ITP
imports "~~/src/HOL/ex/Interpretation_with_Defs"
"~~/src/HOL/Library/While_Combinator"
- Collecting
+ "../Collecting"
begin
subsection "Orderings"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Jul 24 21:48:41 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int1_const_ITP
-imports Abs_Int1_ITP Abs_Int_Tests
+imports Abs_Int1_ITP "../Abs_Int_Tests"
begin
subsection "Constant Propagation"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Tue Jul 24 21:48:41 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ITP
-imports Abs_Int1_ITP Vars
+imports Abs_Int1_ITP "../Vars"
begin
instantiation prod :: (preord,preord) preord
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Jul 24 21:48:41 2012 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int2_ivl_ITP
-imports Abs_Int2_ITP Abs_Int_Tests
+imports Abs_Int2_ITP "../Abs_Int_Tests"
begin
subsection "Interval Analysis"
--- a/src/HOL/IsaMakefile Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 24 21:48:41 2012 +0200
@@ -57,6 +57,7 @@
HOL-Mutabelle \
HOL-NanoJava \
HOL-Nitpick_Examples \
+ HOL-NSA-Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
HOL-Quickcheck_Examples \
--- a/src/HOL/NSA/Examples/NSPrimes.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Tue Jul 24 21:48:41 2012 +0200
@@ -23,10 +23,10 @@
choicefun :: "'a set => 'a" where
"choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)"
-consts injf_max :: "nat => ('a::{order} set) => 'a"
-primrec
+primrec injf_max :: "nat => ('a::{order} set) => 'a"
+where
injf_max_zero: "injf_max 0 E = choicefun E"
- injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
+| injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"
--- a/src/HOL/ROOT Tue Jul 24 12:36:59 2012 +0200
+++ b/src/HOL/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -2,7 +2,7 @@
description {* Classical Higher-order Logic *}
options [document_graph]
theories Complex_Main
- files "document/root.tex" "document/root.bib"
+ files "document/root.bib" "document/root.tex"
session "HOL-Base"! in "." = Pure +
description {* Raw HOL base, with minimal tools *}
@@ -19,11 +19,744 @@
options [document = false]
theories Main
-session "HOL-Proofs"! (2) in "." = Pure +
+session "HOL-Proofs"! (4) in "." = Pure +
description {* HOL-Main with proof terms *}
options [document = false, proofs = 2, parallel_proofs = 0]
theories Main
+session Library = HOL +
+ description {* Classical Higher-order Logic -- batteries included *}
+ theories
+ Library
+ List_Prefix
+ List_lexord
+ Sublist_Order
+ Product_Lattice
+ Code_Char_chr
+ Code_Char_ord
+ Code_Integer
+ Efficient_Nat
+ (*"Code_Prolog" FIXME*)
+ Code_Real_Approx_By_Float
+ Target_Numeral
+ files "document/root.bib" "document/root.tex"
+
+session Hahn_Banach = HOL +
+ description {*
+ Author: Gertrud Bauer, TU Munich
+
+ The Hahn-Banach theorem for real vector spaces.
+ *}
+ options [document_graph]
+ theories Hahn_Banach
+ files "document/root.bib" "document/root.tex"
+
+session Induct = HOL +
+ theories [quick_and_dirty]
+ Common_Patterns
+ theories
+ QuoDataType
+ QuoNestedDataType
+ Term
+ SList
+ ABexp
+ Tree
+ Ordinals
+ Sigma_Algebra
+ Comb
+ PropLog
+ Com
+ files "document/root.tex"
+
+session IMP = HOL +
+ options [document_graph]
+ theories [document = false]
+ "~~/src/HOL/ex/Interpretation_with_Defs"
+ "~~/src/HOL/Library/While_Combinator"
+ "~~/src/HOL/Library/Char_ord"
+ "~~/src/HOL/Library/List_lexord"
+ theories
+ BExp
+ ASM
+ Small_Step
+ Denotation
+ Comp_Rev
+ Poly_Types
+ Sec_Typing
+ Sec_TypingT
+ Def_Ass_Sound_Big
+ Def_Ass_Sound_Small
+ Live
+ Live_True
+ Hoare_Examples
+ VC
+ HoareT
+ Collecting1
+ Collecting_list
+ Abs_Int_Tests
+ Abs_Int1_parity
+ Abs_Int1_const
+ Abs_Int3
+ "Abs_Int_ITP/Abs_Int1_parity_ITP"
+ "Abs_Int_ITP/Abs_Int1_const_ITP"
+ "Abs_Int_ITP/Abs_Int3_ITP"
+ "Abs_Int_Den/Abs_Int_den2"
+ Procs_Dyn_Vars_Dyn
+ Procs_Stat_Vars_Dyn
+ Procs_Stat_Vars_Stat
+ C_like
+ OO
+ Fold
+ files "document/root.bib" "document/root.tex"
+
+session IMPP = HOL +
+ description {*
+ Author: David von Oheimb
+ Copyright 1999 TUM
+ *}
+ options [document = false]
+ theories EvenOdd
+
+session Import = HOL +
+ options [document_graph]
+ theories HOL_Light_Maps
+ theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
+
+session Number_Theory = HOL +
+ options [document = false]
+ theories Number_Theory
+
+session Old_Number_Theory = HOL +
+ options [document_graph]
+ theories [document = false]
+ "~~/src/HOL/Library/Infinite_Set"
+ "~~/src/HOL/Library/Permutation"
+ theories
+ Fib
+ Factorization
+ Chinese
+ WilsonRuss
+ WilsonBij
+ Quadratic_Reciprocity
+ Primes
+ Pocklington
+ files "document/root.tex"
+
+session Hoare = HOL +
+ theories Hoare
+ files "document/root.bib" "document/root.tex"
+
+session Hoare_Parallel = HOL +
+ options [document_graph]
+ theories Hoare_Parallel
+ files "document/root.bib" "document/root.tex"
+
+session Codegenerator_Test = "HOL-Library" +
+ options [document = false, document_graph = false, browser_info = false]
+ theories Generate Generate_Pretty
+
+session Metis_Examples = HOL +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+ Testing Metis and Sledgehammer.
+ *}
+ options [document = false]
+ theories
+ Abstraction
+ Big_O
+ Binary_Tree
+ Clausification
+ Message
+ Proxies
+ Tarski
+ Trans_Closure
+ Sets
+
+session Nitpick_Examples = HOL +
+ description {*
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2009
+ *}
+ options [document = false]
+ theories [quick_and_dirty] Nitpick_Examples
+
+session Algebra = HOL +
+ description {*
+ Author: Clemens Ballarin, started 24 September 1999
+
+ The Isabelle Algebraic Library.
+ *}
+ options [document_graph]
+ theories [document = false]
+ (* Preliminaries from set and number theory *)
+ "~~/src/HOL/Library/FuncSet"
+ "~~/src/HOL/Old_Number_Theory/Primes"
+ "~~/src/HOL/Library/Binomial"
+ "~~/src/HOL/Library/Permutation"
+ theories
+ (*** New development, based on explicit structures ***)
+ (* Groups *)
+ FiniteProduct (* Product operator for commutative groups *)
+ Sylow (* Sylow's theorem *)
+ Bij (* Automorphism Groups *)
+
+ (* Rings *)
+ Divisibility (* Rings *)
+ IntRing (* Ideals and residue classes *)
+ UnivPoly (* Polynomials *)
+ theories [document = false]
+ (*** Old development, based on axiomatic type classes ***)
+ "abstract/Abstract" (*The ring theory*)
+ "poly/Polynomial" (*The full theory*)
+ files "document/root.bib" "document/root.tex"
+
+session Auth = HOL +
+ options [document_graph]
+ theories
+ Auth_Shared
+ Auth_Public
+ "Smartcard/Auth_Smartcard"
+ "Guard/Auth_Guard_Shared"
+ "Guard/Auth_Guard_Public"
+ files "document/root.tex"
+
+session UNITY = HOL +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+ Verifying security protocols using UNITY.
+ *}
+ options [document_graph]
+ theories [document = false] "../Auth/Public"
+ theories
+ (*Basic meta-theory*)
+ "UNITY_Main"
+
+ (*Simple examples: no composition*)
+ "Simple/Deadlock"
+ "Simple/Common"
+ "Simple/Network"
+ "Simple/Token"
+ "Simple/Channel"
+ "Simple/Lift"
+ "Simple/Mutex"
+ "Simple/Reach"
+ "Simple/Reachability"
+
+ (*Verifying security protocols using UNITY*)
+ "Simple/NSP_Bad"
+
+ (*Example of composition*)
+ "Comp/Handshake"
+
+ (*Universal properties examples*)
+ "Comp/Counter"
+ "Comp/Counterc"
+ "Comp/Priority"
+
+ "Comp/TimerArray"
+ "Comp/Progress"
+
+ "Comp/Alloc"
+ "Comp/AllocImpl"
+ "Comp/Client"
+
+ (*obsolete*)
+ "ELT"
+ files "document/root.tex"
+
+session Unix = HOL +
+ options [print_mode = "no_brackets,no_type_brackets"]
+ theories Unix
+ files "document/root.bib" "document/root.tex"
+
+session ZF = HOL +
+ description {* *}
+ theories MainZF Games
+ files "document/root.tex"
+
+session Imperative_HOL = HOL +
+ description {* *}
+ options [document_graph, print_mode = "iff,no_brackets"]
+ theories [document = false]
+ "~~/src/HOL/Library/Countable"
+ "~~/src/HOL/Library/Monad_Syntax"
+ "~~/src/HOL/Library/Code_Natural"
+ "~~/src/HOL/Library/LaTeXsugar"
+ theories Imperative_HOL_ex
+ files "document/root.bib" "document/root.tex"
+
+session Decision_Procs = HOL +
+ options [document = false]
+ theories Decision_Procs
+
+session ex in "Proofs/ex" = "HOL-Proofs" +
+ options [document = false, proofs = 2, parallel_proofs = 0]
+ theories Hilbert_Classical
+
+session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
+ description {* Examples for program extraction in Higher-Order Logic *}
+ options [proofs = 2, parallel_proofs = 0]
+ theories [document = false]
+ "~~/src/HOL/Library/Efficient_Nat"
+ "~~/src/HOL/Library/Monad_Syntax"
+ "~~/src/HOL/Number_Theory/Primes"
+ "~~/src/HOL/Number_Theory/UniqueFactorization"
+ "~~/src/HOL/Library/State_Monad"
+ theories
+ Greatest_Common_Divisor
+ Warshall
+ Higman_Extraction
+ Pigeonhole
+ Euclid
+ files "document/root.bib" "document/root.tex"
+
+session Lambda in "Proofs/Lambda" = "HOL-Proofs" +
+ options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
+ theories [document = false]
+ "~~/src/HOL/Library/Code_Integer"
+ theories
+ Eta
+ StrongNorm
+ Standardization
+ WeakNorm
+ files "document/root.bib" "document/root.tex"
+
+session Prolog = HOL +
+ description {*
+ Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+ *}
+ options [document = false]
+ theories Test Type
+
+session MicroJava = HOL +
+ options [document_graph]
+ theories [document = false] "~~/src/HOL/Library/While_Combinator"
+ theories MicroJava
+ files
+ "document/introduction.tex"
+ "document/root.bib"
+ "document/root.tex"
+
+session NanoJava = HOL +
+ options [document_graph]
+ theories Example
+ files "document/root.bib" "document/root.tex"
+
+session Bali = HOL +
+ options [document_graph]
+ theories
+ AxExample
+ AxSound
+ AxCompl
+ Trans
+ files "document/root.tex"
+
+session IOA = HOL +
+ description {*
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+ The meta theory of I/O-Automata.
+
+ @inproceedings{Nipkow-Slind-IOA,
+ author={Tobias Nipkow and Konrad Slind},
+ title={{I/O} Automata in {Isabelle/HOL}},
+ booktitle={Proc.\ TYPES Workshop 1994},
+ publisher=Springer,
+ series=LNCS,
+ note={To appear}}
+ ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
+
+ and
+
+ @inproceedings{Mueller-Nipkow,
+ author={Olaf M\"uller and Tobias Nipkow},
+ title={Combining Model Checking and Deduction for {I/O}-Automata},
+ booktitle={Proc.\ TACAS Workshop},
+ organization={Aarhus University, BRICS report},
+ year=1995}
+ ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
+ *}
+ options [document = false]
+ theories Solve
+
+session Lattice = HOL +
+ description {*
+ Author: Markus Wenzel, TU Muenchen
+
+ Basic theory of lattices and orders.
+ *}
+ theories CompleteLattice
+ files "document/root.tex"
+
+session ex = HOL +
+ description {* Miscellaneous examples for Higher-Order Logic. *}
+ theories [document = false]
+ "~~/src/HOL/Library/State_Monad"
+ Code_Nat_examples
+ "~~/src/HOL/Library/FuncSet"
+ Eval_Examples
+ Normalization_by_Evaluation
+ Hebrew
+ Chinese
+ Serbian
+ "~~/src/HOL/Library/FinFun_Syntax"
+ theories
+ Iff_Oracle
+ Coercion_Examples
+ Numeral_Representation
+ Higher_Order_Logic
+ Abstract_NAT
+ Guess
+ Binary
+ Fundefs
+ Induction_Schema
+ LocaleTest2
+ Records
+ While_Combinator_Example
+ MonoidGroup
+ BinEx
+ Hex_Bin_Examples
+ Antiquote
+ Multiquote
+ PER
+ NatSum
+ ThreeDivides
+ Intuitionistic
+ CTL
+ Arith_Examples
+ BT
+ Tree23
+ MergeSort
+ Lagrange
+ Groebner_Examples
+ MT
+ Unification
+ Primrec
+ Tarski
+ Classical
+ Set_Theory
+ Meson_Test
+ Termination
+ Coherent
+ PresburgerEx
+ ReflectionEx
+ Sqrt
+ Sqrt_Script
+ Transfer_Ex
+ Transfer_Int_Nat
+ HarmonicSeries
+ Refute_Examples
+ Landau
+ Execute_Choice
+ Summation
+ Gauge_Integration
+ Dedekind_Real
+ Quicksort
+ Birthday_Paradox
+ List_to_Set_Comprehension_Examples
+ Seq
+ Simproc_Tests
+ Executable_Relation
+ FinFunPred
+ Set_Comprehension_Pointfree_Tests
+ Parallel_Example
+ theories SVC_Oracle
+ theories [condition = SVC_HOME] svc_test
+ theories [condition = ZCHAFF_HOME]
+ (*requires zChaff (or some other reasonably fast SAT solver)*)
+ Sudoku
+(* FIXME
+(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
+(*global side-effects ahead!*)
+try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)
+*)
+ files "document/root.bib" "document/root.tex"
+
+session Isar_Examples = HOL +
+ description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
+ theories [document = false]
+ "~~/src/HOL/Library/Lattice_Syntax"
+ "../Number_Theory/Primes"
+ theories
+ Basic_Logic
+ Cantor
+ Drinker
+ Expr_Compiler
+ Fibonacci
+ Group
+ Group_Context
+ Group_Notepad
+ Hoare_Ex
+ Knaster_Tarski
+ Mutilated_Checkerboard
+ Nested_Datatype
+ Peirce
+ Puzzle
+ Summation
+ files
+ "document/root.bib"
+ "document/root.tex"
+ "document/style.tex"
+
+session SET_Protocol = HOL +
+ options [document_graph]
+ theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
+ theories SET_Protocol
+ files "document/root.tex"
+
+session Matrix_LP = HOL +
+ options [document_graph]
+ theories Cplex
+ files "document/root.tex"
+
+session TLA! = HOL +
+ description {* The Temporal Logic of Actions *}
+ options [document = false]
+ theories TLA
+
+session Inc in "TLA/Inc" = TLA +
+ options [document = false]
+ theories Inc
+
+session Buffer in "TLA/Buffer" = TLA +
+ options [document = false]
+ theories DBuffer
+
+session Memory in "TLA/Memory" = TLA +
+ options [document = false]
+ theories MemoryImplementation
+
+session TPTP = HOL +
+ description {*
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Nik Sultana, University of Cambridge
+ Copyright 2011
+
+ TPTP-related extensions.
+ *}
+ options [document = false]
+ theories
+ ATP_Theory_Export
+ MaSh_Eval
+ MaSh_Export
+ TPTP_Interpret
+ THF_Arith
+ theories [proofs = 0] (* FIXME !? *)
+ ATP_Problem_Import
+
+session Multivariate_Analysis = HOL +
+ options [document_graph]
+ theories
+ Multivariate_Analysis
+ Determinants
+ files
+ "Integration.certs"
+ "document/root.tex"
+
+session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
+ options [document_graph]
+ theories [document = false]
+ "~~/src/HOL/Library/Countable"
+ "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
+ "~~/src/HOL/Library/Permutation"
+ theories
+ Probability
+ "ex/Dining_Cryptographers"
+ "ex/Koepf_Duermuth_Countermeasure"
+ files "document/root.tex"
+
+session Nominal (2) = HOL +
+ options [document = false]
+ theories Nominal
+
+session Examples in "Nominal/Examples" = "HOL-Nominal" +
+ options [document = false]
+ theories Nominal_Examples
+ theories [quick_and_dirty] VC_Condition
+
+session Word = HOL +
+ options [document_graph]
+ theories Word
+ files "document/root.bib" "document/root.tex"
+
+session Examples in "Word/Examples" = "HOL-Word" +
+ options [document = false]
+ theories WordExamples
+
+session Statespace = HOL +
+ theories StateSpaceEx
+ files "document/root.tex"
+
+session NSA = HOL +
+ options [document_graph]
+ theories Hypercomplex
+ files "document/root.tex"
+
+session Examples in "NSA/Examples" = "HOL-NSA" +
+ options [document = false]
+ theories NSPrimes
+
+session Mirabelle = HOL +
+ options [document = false]
+ theories Mirabelle_Test
+(* FIXME
+ @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
+*)
+
+session SMT_Examples = "HOL-Word" +
+ options [document = false, quick_and_dirty]
+ theories
+ SMT_Tests
+ SMT_Examples
+ SMT_Word_Examples
+ files
+ "SMT_Examples.certs"
+ "SMT_Tests.certs"
+
+session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+ options [document = false]
+ theories Boogie
+ (* FIXME files!?! *)
+
+session Examples in "Boogie/Examples" = "HOL-Boogie" +
+ options [document = false]
+ theories
+ Boogie_Max_Stepwise
+ Boogie_Max
+ Boogie_Dijkstra
+ VCC_Max
+ files
+ "Boogie_Dijkstra.certs"
+ "Boogie_Max.certs"
+ "VCC_Max.certs"
+
+session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+ options [document = false]
+ theories SPARK
+
+session Examples in "SPARK/Examples" = "HOL-SPARK" +
+ options [document = false]
+ theories
+ "Gcd/Greatest_Common_Divisor"
+
+ "Liseq/Longest_Increasing_Subsequence"
+
+ "RIPEMD-160/F"
+ "RIPEMD-160/Hash"
+ "RIPEMD-160/K_L"
+ "RIPEMD-160/K_R"
+ "RIPEMD-160/R_L"
+ "RIPEMD-160/Round"
+ "RIPEMD-160/R_R"
+ "RIPEMD-160/S_L"
+ "RIPEMD-160/S_R"
+
+ "Sqrt/Sqrt"
+ files
+ "Gcd/greatest_common_divisor/g_c_d.fdl"
+ "Gcd/greatest_common_divisor/g_c_d.rls"
+ "Gcd/greatest_common_divisor/g_c_d.siv"
+ "Liseq/liseq/liseq_length.fdl"
+ "Liseq/liseq/liseq_length.rls"
+ "Liseq/liseq/liseq_length.siv"
+ "RIPEMD-160/rmd/f.fdl"
+ "RIPEMD-160/rmd/f.rls"
+ "RIPEMD-160/rmd/f.siv"
+ "RIPEMD-160/rmd/hash.fdl"
+ "RIPEMD-160/rmd/hash.rls"
+ "RIPEMD-160/rmd/hash.siv"
+ "RIPEMD-160/rmd/k_l.fdl"
+ "RIPEMD-160/rmd/k_l.rls"
+ "RIPEMD-160/rmd/k_l.siv"
+ "RIPEMD-160/rmd/k_r.fdl"
+ "RIPEMD-160/rmd/k_r.rls"
+ "RIPEMD-160/rmd/k_r.siv"
+ "RIPEMD-160/rmd/r_l.fdl"
+ "RIPEMD-160/rmd/r_l.rls"
+ "RIPEMD-160/rmd/r_l.siv"
+ "RIPEMD-160/rmd/round.fdl"
+ "RIPEMD-160/rmd/round.rls"
+ "RIPEMD-160/rmd/round.siv"
+ "RIPEMD-160/rmd/r_r.fdl"
+ "RIPEMD-160/rmd/r_r.rls"
+ "RIPEMD-160/rmd/r_r.siv"
+ "RIPEMD-160/rmd/s_l.fdl"
+ "RIPEMD-160/rmd/s_l.rls"
+ "RIPEMD-160/rmd/s_l.siv"
+ "RIPEMD-160/rmd/s_r.fdl"
+ "RIPEMD-160/rmd/s_r.rls"
+ "RIPEMD-160/rmd/s_r.siv"
+
+session Manual in "SPARK/Manual" = "HOL-SPARK" +
+ options [show_question_marks = false]
+ theories
+ Example_Verification
+ VC_Principles
+ Reference
+ Complex_Types
+ files
+ "complex_types_app/initialize.fdl"
+ "complex_types_app/initialize.rls"
+ "complex_types_app/initialize.siv"
+ "document/complex_types.ads"
+ "document/complex_types_app.adb"
+ "document/complex_types_app.ads"
+ "document/Gcd.adb"
+ "document/Gcd.ads"
+ "document/intro.tex"
+ "document/loop_invariant.adb"
+ "document/loop_invariant.ads"
+ "document/root.bib"
+ "document/root.tex"
+ "document/Simple_Gcd.adb"
+ "document/Simple_Gcd.ads"
+ "loop_invariant/proc1.fdl"
+ "loop_invariant/proc1.rls"
+ "loop_invariant/proc1.siv"
+ "loop_invariant/proc2.fdl"
+ "loop_invariant/proc2.rls"
+ "loop_invariant/proc2.siv"
+ "simple_greatest_common_divisor/g_c_d.fdl"
+ "simple_greatest_common_divisor/g_c_d.rls"
+ "simple_greatest_common_divisor/g_c_d.siv"
+
+session Mutabelle = HOL +
+ options [document = false]
+ theories MutabelleExtra
+
+session Quickcheck_Examples = HOL +
+ options [document = false]
+ theories Quickcheck_Examples (* FIXME *)
+
+session Quotient_Examples = HOL +
+ description {*
+ Author: Cezary Kaliszyk and Christian Urban
+ *}
+ options [document = false]
+ theories
+ DList
+ FSet
+ Quotient_Int
+ Quotient_Message
+ Lift_FSet
+ Lift_Set
+ Lift_RBT
+ Lift_Fun
+ Quotient_Rat
+ Lift_DList
+
+session Predicate_Compile_Examples = HOL +
+ options [document = false]
+ theories (* FIXME *)
+ Examples
+ Predicate_Compile_Tests
+ Specialisation_Examples
+
session HOLCF! (3) = HOL +
description {*
Author: Franz Regensburger
@@ -35,6 +768,111 @@
theories [document = false]
"~~/src/HOL/Library/Nat_Bijection"
"~~/src/HOL/Library/Countable"
- theories Plain_HOLCF Fixrec HOLCF
+ theories
+ Plain_HOLCF
+ Fixrec
+ HOLCF
+ files "document/root.tex"
+
+session Tutorial in "HOLCF/Tutorial" = HOLCF +
+ theories
+ Domain_ex
+ Fixrec_ex
+ New_Domain
+ files "document/root.tex"
+
+session Library in "HOLCF/Library" = HOLCF +
+ options [document = false]
+ theories HOLCF_Library
+
+session IMP in "HOLCF/IMP" = HOLCF +
+ options [document = false]
+ theories HoareEx
files "document/root.tex"
+session ex in "HOLCF/ex" = HOLCF +
+ description {* Misc HOLCF examples *}
+ options [document = false]
+ theories
+ Dnat
+ Dagstuhl
+ Focus_ex
+ Fix2
+ Hoare
+ Concurrency_Monad
+ Loop
+ Powerdomain_ex
+ Domain_Proofs
+ Letrec
+ Pattern_Match
+
+session FOCUS in "HOLCF/FOCUS" = HOLCF +
+ options [document = false]
+ theories
+ Fstreams
+ FOCUS
+ Buffer_adm
+
+session IOA! in "HOLCF/IOA" = HOLCF +
+ description {*
+ Author: Olaf Mueller
+
+ Formalization of a semantic model of I/O-Automata.
+ *}
+ options [document = false]
+ theories "meta_theory/Abstraction"
+
+session ABP in "HOLCF/IOA/ABP" = IOA +
+ description {*
+ Author: Olaf Mueller
+
+ The Alternating Bit Protocol performed in I/O-Automata.
+ *}
+ options [document = false]
+ theories Correctness
+
+session NTP in "HOLCF/IOA/NTP" = IOA +
+ description {*
+ Author: Tobias Nipkow & Konrad Slind
+
+ A network transmission protocol, performed in the
+ I/O automata formalization by Olaf Mueller.
+ *}
+ options [document = false]
+ theories Correctness
+
+session Storage in "HOLCF/IOA/Storage" = IOA +
+ description {*
+ Author: Olaf Mueller
+
+ Memory storage case study.
+ *}
+ options [document = false]
+ theories Correctness
+
+session ex in "HOLCF/IOA/ex" = IOA +
+ description {*
+ Author: Olaf Mueller
+ *}
+ options [document = false]
+ theories
+ TrivEx
+ TrivEx2
+
+session Datatype_Benchmark = HOL +
+ description {* Some rather large datatype examples (from John Harrison). *}
+ options [document = false]
+ theories [condition = ISABELLE_BENCHMARK]
+ (* FIXME Toplevel.timing := true; *)
+ Brackin
+ Instructions
+ SML
+ Verilog
+
+session Record_Benchmark = HOL +
+ description {* Some benchmark on large record. *}
+ options [document = false]
+ theories [condition = ISABELLE_BENCHMARK]
+ (* FIXME Toplevel.timing := true; *)
+ Record_Benchmark
+
--- a/src/LCF/LCF.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/LCF/LCF.thy Tue Jul 24 21:48:41 2012 +0200
@@ -6,7 +6,7 @@
header {* LCF on top of First-Order Logic *}
theory LCF
-imports FOL
+imports "~~/src/FOL/FOL"
begin
text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,22 @@
+session LCF! in "." = Pure +
+ description {*
+ Author: Tobias Nipkow
+ Copyright 1992 University of Cambridge
+ *}
+ options [document = false]
+ theories LCF
+
+session ex = LCF +
+ description {*
+ Author: Tobias Nipkow
+ Copyright 1991 University of Cambridge
+
+ Some examples from Lawrence Paulson's book Logic and Computation.
+ *}
+ options [document = false]
+ theories
+ Ex1
+ Ex2
+ Ex3
+ Ex4
+
--- a/src/Pure/General/exn.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/General/exn.scala Tue Jul 24 21:48:41 2012 +0200
@@ -31,11 +31,19 @@
private val runtime_exception = Class.forName("java.lang.RuntimeException")
- def message(exn: Throwable): String =
- if (exn.getClass == runtime_exception) {
+ def user_message(exn: Throwable): Option[String] =
+ if (exn.isInstanceOf[java.io.IOException]) {
+ val msg = exn.getMessage
+ Some(if (msg == null) "I/O error" else "I/O error: " + msg)
+ }
+ else if (exn.getClass == runtime_exception) {
val msg = exn.getMessage
- if (msg == null) "Error" else msg
+ Some(if (msg == null) "Error" else msg)
}
- else exn.toString
+ else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
+ else None
+
+ def message(exn: Throwable): String =
+ user_message(exn) getOrElse exn.toString
}
--- a/src/Pure/General/path.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/General/path.scala Tue Jul 24 21:48:41 2012 +0200
@@ -96,8 +96,16 @@
new Path(norm_elems(explode_elems(raw_elems) ++ roots))
}
+ def is_ok(str: String): Boolean =
+ try { explode(str); true } catch { case ERROR(_) => false }
+
def split(str: String): List[Path] =
space_explode(':', str).filterNot(_.isEmpty).map(explode)
+
+
+ /* encode */
+
+ val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
}
--- a/src/Pure/IsaMakefile Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/IsaMakefile Tue Jul 24 21:48:41 2012 +0200
@@ -188,11 +188,12 @@
Syntax/syntax_phases.ML \
Syntax/syntax_trans.ML \
Syntax/term_position.ML \
+ System/build.ML \
System/invoke_scala.ML \
- System/build.ML \
System/isabelle_process.ML \
System/isabelle_system.ML \
System/isar.ML \
+ System/options.ML \
System/session.ML \
System/system_channel.ML \
Thy/html.ML \
--- a/src/Pure/Isar/parse.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/Isar/parse.scala Tue Jul 24 21:48:41 2012 +0200
@@ -60,7 +60,10 @@
def text: Parser[String] = atom("text", _.is_text)
def ML_source: Parser[String] = atom("ML source", _.is_text)
def doc_source: Parser[String] = atom("document source", _.is_text)
- def path: Parser[String] = atom("file name/path specification", _.is_name)
+ def path: Parser[String] =
+ atom("file name/path specification", tok => tok.is_name && Path.is_ok(tok.content))
+ def theory_name: Parser[String] =
+ atom("theory name", tok => tok.is_name && Thy_Load.is_ok(tok.content))
private def tag_name: Parser[String] =
atom("tag name", tok =>
--- a/src/Pure/ROOT.ML Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/ROOT.ML Tue Jul 24 21:48:41 2012 +0200
@@ -103,6 +103,7 @@
use "context.ML";
use "context_position.ML";
use "config.ML";
+use "System/options.ML";
(* inner syntax *)
--- a/src/Pure/System/build.ML Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/System/build.ML Tue Jul 24 21:48:41 2012 +0200
@@ -12,18 +12,64 @@
structure Build: BUILD =
struct
+local
+
+fun use_thys options =
+ Thy_Info.use_thys
+ |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
+ |> Unsynchronized.setmp print_mode
+ (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+ |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+ |> Unsynchronized.setmp Goal.parallel_proofs_threshold
+ (Options.int options "parallel_proofs_threshold")
+ |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+ |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+ |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
+ Present.no_document
+ |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
+ |> Unsynchronized.setmp Printer.show_question_marks_default
+ (Options.bool options "show_question_marks")
+ |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
+ |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
+ |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique");
+
+fun use_theories (options, thys) =
+ let val condition = space_explode "," (Options.string options "condition") in
+ (case filter_out (can getenv_strict) condition of
+ [] => use_thys options thys
+ | conds =>
+ Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
+ " (undefined " ^ commas conds ^ ")\n"))
+ end;
+
+in
+
fun build args_file =
let
- val (save, (parent, (name, theories))) =
+ val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
+ (name, (base_name, theories)))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
- let open XML.Decode in pair bool (pair string (pair string (list string))) end;
+ let open XML.Decode in
+ pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
+ (pair string (pair string ((list (pair Options.decode (list string)))))))))))
+ end;
- val _ = Session.init false parent name; (* FIXME reset!? *)
- val _ = Thy_Info.use_thys theories;
+ val _ =
+ Session.init save false
+ (Options.bool options "browser_info") browser_info
+ (Options.string options "document")
+ (Options.bool options "document_graph")
+ (space_explode ":" (Options.string options "document_variants"))
+ parent_base_name base_name
+ (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
+ (Options.string options "browser_info_remote")
+ verbose;
+ val _ = Session.with_timing name timing (List.app use_theories) theories;
val _ = Session.finish ();
-
val _ = if save then () else quit ();
in () end
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
end;
+
+end;
--- a/src/Pure/System/build.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/System/build.scala Tue Jul 24 21:48:41 2012 +0200
@@ -42,8 +42,10 @@
/* Info */
sealed case class Info(
+ base_name: String,
dir: Path,
parent: Option[String],
+ parent_base_name: Option[String],
description: String,
options: Options,
theories: List[(Options, List[Path])],
@@ -115,7 +117,7 @@
private case class Session_Entry(
name: String,
- reset: Boolean,
+ this_name: Boolean,
order: Int,
path: Option[String],
parent: Option[String],
@@ -140,7 +142,6 @@
val session_entry: Parser[Session_Entry] =
{
val session_name = atom("session name", _.is_name)
- val theory_name = atom("theory name", _.is_name)
val option =
name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
@@ -187,16 +188,19 @@
try {
if (entry.name == "") error("Bad session name")
- val full_name =
+ val (full_name, parent_base_name) =
if (is_pure(entry.name)) {
if (entry.parent.isDefined) error("Illegal parent session")
- else entry.name
+ else (entry.name, None: Option[String])
}
else
entry.parent match {
case Some(parent_name) if queue1.defined(parent_name) =>
- if (entry.reset) entry.name
- else parent_name + "-" + entry.name
+ val full_name =
+ if (entry.this_name) entry.name
+ else parent_name + "-" + entry.name
+ val parent_base_name = Some(queue1(parent_name).base_name)
+ (full_name, parent_base_name)
case _ => error("Bad parent session")
}
@@ -208,14 +212,17 @@
val key = Session.Key(full_name, entry.order)
+ val session_options = options ++ entry.options
+
val theories =
- entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
+ entry.theories.map({ case (opts, thys) =>
+ (session_options ++ opts, thys.map(Path.explode(_))) })
val files = entry.files.map(Path.explode(_))
val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
val info =
- Session.Info(dir + path, entry.parent,
- entry.description, options ++ entry.options, theories, files, digest)
+ Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
+ entry.description, session_options, theories, files, digest)
queue1 + (key, info)
}
@@ -279,6 +286,10 @@
/** build **/
+ private def echo(msg: String) { java.lang.System.out.println(msg) }
+ private def sleep(): Unit = Thread.sleep(500)
+
+
/* dependencies */
sealed case class Node(
@@ -290,7 +301,7 @@
def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
}
- def dependencies(queue: Session.Queue): Deps =
+ def dependencies(verbose: Boolean, queue: Session.Queue): Deps =
Deps((Map.empty[String, Node] /: queue.topological_order)(
{ case (deps, (name, info)) =>
val preloaded =
@@ -300,6 +311,8 @@
}
val thy_info = new Thy_Info(new Thy_Load(preloaded))
+ if (verbose) echo("Checking " + name)
+
val thy_deps =
thy_info.dependencies(
info.theories.map(_._2).flatten.
@@ -318,7 +331,12 @@
}
thy :: uses
}).flatten ::: info.files.map(file => info.dir + file)
- val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
+ val sources =
+ try { all_files.map(p => (p, SHA1.digest(p))) }
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session " + quote(name))
+ }
deps + (name -> Node(loaded_theories, sources))
}))
@@ -340,9 +358,23 @@
def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
}
- private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
+ private def start_job(name: String, info: Session.Info, output: Option[String],
+ options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
{
+ // global browser info dir
+ if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
+ {
+ browser_info.file.mkdirs()
+ File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+ browser_info + Path.explode("isabelle.gif"))
+ File.write(browser_info + Path.explode("index.html"),
+ File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+ }
+
val parent = info.parent.getOrElse("")
+ val parent_base_name = info.parent_base_name.getOrElse("")
val cwd = info.dir.file
val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
@@ -371,8 +403,10 @@
val args_xml =
{
import XML.Encode._
- pair(bool, pair(string, pair(string, list(string))))(
- output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
+ pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
+ pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
+ (output.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
+ (name, (info.base_name, info.theories)))))))))
}
new Job(cwd, env, script, YXML.string_of_body(args_xml))
}
@@ -380,33 +414,18 @@
/* build */
- private def echo(msg: String) { java.lang.System.out.println(msg) }
- private def sleep(): Unit = Thread.sleep(500)
-
def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
- list_only: Boolean, system_mode: Boolean, verbose: Boolean,
+ no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
{
val options = (Options.init() /: more_options)(_.define_simple(_))
val queue = find_sessions(options, all_sessions, sessions, more_dirs)
- val deps = dependencies(queue)
+ val deps = dependencies(verbose, queue)
val (output_dir, browser_info) =
if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
- // prepare browser info dir
- if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
- {
- browser_info.file.mkdirs()
- File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
- browser_info + Path.explode("isabelle.gif"))
- File.write(browser_info + Path.explode("index.html"),
- File.read(Path.explode("~~/lib/html/library_index_header.template")) +
- File.read(Path.explode("~~/lib/html/library_index_content.template")) +
- File.read(Path.explode("~~/lib/html/library_index_footer.template")))
- }
-
// prepare log dir
val log_dir = output_dir + Path.explode("log")
log_dir.file.mkdirs()
@@ -444,8 +463,7 @@
else if (running.size < (max_jobs max 1)) {
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
- if (list_only) {
- echo(name + " in " + info.dir)
+ if (no_build) {
loop(pending - name, running, results + (name -> 0))
}
else if (info.parent.map(results(_)).forall(_ == 0)) {
@@ -454,7 +472,7 @@
Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
else None
echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
- val job = start_job(name, info, output)
+ val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
loop(pending, running + (name -> job), results)
}
else {
@@ -467,7 +485,13 @@
else { sleep(); loop(pending, running, results) }
}
- (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
+ val results = loop(queue, Map.empty, Map.empty)
+ val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
+ if (rc != 0) {
+ val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
+ echo("Unfinished session(s): " + commas(unfinished))
+ }
+ rc
}
@@ -481,11 +505,12 @@
Properties.Value.Boolean(all_sessions) ::
Properties.Value.Boolean(build_images) ::
Properties.Value.Int(max_jobs) ::
- Properties.Value.Boolean(list_only) ::
+ Properties.Value.Boolean(no_build) ::
Properties.Value.Boolean(system_mode) ::
+ Properties.Value.Boolean(timing) ::
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(more_dirs, options, sessions) =>
- build(all_sessions, build_images, max_jobs, list_only, system_mode,
+ build(all_sessions, build_images, max_jobs, no_build, system_mode, timing,
verbose, more_dirs.map(Path.explode), options, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/options.ML Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,76 @@
+(* Title: Pure/System/options.ML
+ Author: Makarius
+
+Stand-alone options with external string representation.
+*)
+
+signature OPTIONS =
+sig
+ type T
+ val empty: T
+ val bool: T -> string -> bool
+ val int: T -> string -> int
+ val real: T -> string -> real
+ val string: T -> string -> string
+ val declare: {name: string, typ: string, value: string} -> T -> T
+ val decode: XML.body -> T
+end;
+
+structure Options: OPTIONS =
+struct
+
+(* representation *)
+
+val boolT = "bool";
+val intT = "int";
+val realT = "real";
+val stringT = "string";
+
+datatype T = Options of {typ: string, value: string} Symtab.table;
+
+val empty = Options Symtab.empty;
+
+
+(* get *)
+
+fun get T parse (Options tab) name =
+ (case Symtab.lookup tab name of
+ SOME {typ, value} =>
+ if typ = T then
+ (case parse value of
+ SOME x => x
+ | NONE =>
+ error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
+ else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
+ | NONE => error ("Unknown option " ^ quote name));
+
+val bool = get boolT Bool.fromString;
+val int = get intT Int.fromString;
+val real = get realT Real.fromString;
+val string = get stringT SOME;
+
+
+(* declare *)
+
+fun declare {name, typ, value} (Options tab) =
+ let
+ val check_value =
+ if typ = boolT then ignore oo bool
+ else if typ = intT then ignore oo int
+ else if typ = realT then ignore oo real
+ else if typ = stringT then ignore oo string
+ else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
+ val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
+ handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
+ val _ = check_value options' name;
+ in options' end;
+
+
+(* decode *)
+
+fun decode body =
+ fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
+ (let open XML.Decode in list (triple string string string) end body) empty;
+
+end;
+
--- a/src/Pure/System/options.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/System/options.scala Tue Jul 24 21:48:41 2012 +0200
@@ -79,6 +79,11 @@
}
options
}
+
+
+ /* encode */
+
+ val encode: XML.Encode.T[Options] = (options => options.encode)
}
@@ -177,7 +182,7 @@
case "int" => Options.Int
case "real" => Options.Real
case "string" => Options.String
- case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
+ case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
}
(new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
}
@@ -209,4 +214,14 @@
case i => define(str.substring(0, i), str.substring(i + 1))
}
}
+
+
+ /* encode */
+
+ def encode: XML.Body =
+ {
+ import XML.Encode.{string => str, _}
+ list(triple(str, str, str))(
+ options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) }))
+ }
}
--- a/src/Pure/System/session.ML Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/System/session.ML Tue Jul 24 21:48:41 2012 +0200
@@ -9,11 +9,13 @@
val id: unit -> string list
val name: unit -> string
val welcome: unit -> string
- val init: bool -> string -> string -> unit
+ val finish: unit -> unit
+ val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
+ string -> string -> bool * string -> string -> bool -> unit
+ val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
string -> bool -> string list -> string -> string -> bool * string ->
string -> int -> bool -> bool -> int -> int -> int -> int -> unit
- val finish: unit -> unit
end;
structure Session: SESSION =
@@ -63,9 +65,9 @@
end;
-(* init *)
+(* init_name *)
-fun init reset parent name =
+fun init_name reset parent name =
if not (member (op =) (! session) parent) orelse not (! session_finished) then
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
else (add_path reset name; session_finished := false);
@@ -94,26 +96,32 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
+fun with_timing _ false f x = f x
+ | with_timing item true f x =
+ let
+ val start = Timing.start ();
+ val y = f x;
+ val timing = Timing.result start;
+ val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
+ |> Real.fmt (StringCvt.FIX (SOME 2));
+ val _ =
+ Output.physical_stderr ("Timing " ^ item ^ " (" ^
+ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
+ Timing.message timing ^ ", factor " ^ factor ^ ")\n");
+ in y end;
+
+fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
+ (init_name reset parent name;
+ Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
+ (path ()) name (dumping dump) (get_rpath rpath) verbose
+ (map Thy_Info.get_theory (Thy_Info.get_names ())));
+
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
- (init reset parent name;
- Present.init build info info_path doc doc_graph doc_variants (path ()) name
- (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
- if timing then
- let
- val start = Timing.start ();
- val _ = use root;
- val timing = Timing.result start;
- val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
- |> Real.fmt (StringCvt.FIX (SOME 2));
- val _ =
- Output.physical_stderr ("Timing " ^ item ^ " (" ^
- string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
- Timing.message timing ^ ", factor " ^ factor ^ ")\n");
- in () end
- else use root;
+ (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
+ with_timing item timing use root;
finish ()))
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
--- a/src/Pure/Thy/thy_header.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Jul 24 21:48:41 2012 +0200
@@ -46,7 +46,6 @@
val header: Parser[Thy_Header] =
{
val file_name = atom("file name", _.is_name)
- val theory_name = atom("theory name", _.is_name)
val keyword_kind =
atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
--- a/src/Pure/Thy/thy_load.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala Tue Jul 24 21:48:41 2012 +0200
@@ -13,6 +13,10 @@
object Thy_Load
{
def thy_path(path: Path): Path = path.ext("thy")
+
+ def is_ok(str: String): Boolean =
+ try { thy_path(Path.explode(str)); true }
+ catch { case ERROR(_) => false }
}
--- a/src/Pure/library.scala Tue Jul 24 12:36:59 2012 +0200
+++ b/src/Pure/library.scala Tue Jul 24 21:48:41 2012 +0200
@@ -24,11 +24,7 @@
object ERROR
{
def apply(message: String): Throwable = new RuntimeException(message)
- def unapply(exn: Throwable): Option[String] =
- exn match {
- case e: RuntimeException => Some(Exn.message(e))
- case _ => None
- }
+ def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
}
def error(message: String): Nothing = throw ERROR(message)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -0,0 +1,32 @@
+session Sequents! in "." = Pure +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+ Classical Sequent Calculus based on Pure Isabelle.
+ *}
+ options [document = false]
+ theories
+ LK
+ ILL
+ ILL_predlog
+ Washing
+ Modal0
+ T
+ S4
+ S43
+
+session LK = Sequents +
+ description {*
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+ Examples for Classical Logic.
+ *}
+ options [document = false]
+ theories
+ Propositional
+ Quantifiers
+ Hard_Quantifiers
+ Nat
+
--- a/src/ZF/ROOT Tue Jul 24 12:36:59 2012 +0200
+++ b/src/ZF/ROOT Tue Jul 24 21:48:41 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! (10) in "." = FOL +
+session ZF! in "." = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -8,7 +8,9 @@
This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
*}
options [document_graph]
- theories Main Main_ZFC
+ theories
+ Main
+ Main_ZFC
files "document/root.tex"
session AC = ZF +
@@ -19,8 +21,17 @@
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
+ 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 +
@@ -39,6 +50,7 @@
Jacob Frost, A Case Study of Co_induction in Isabelle
Report, Computer Lab, University of Cambridge (1995).
*}
+ options [document = false]
theories ECR
session Constructible = ZF +
@@ -61,6 +73,7 @@
Glynn Winskel. The Formal Semantics of Programming Languages.
MIT Press, 1993.
*}
+ options [document = false]
theories Equiv
files "document/root.tex" "document/root.bib"
@@ -108,6 +121,7 @@
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
J. Functional Programming 4(3) 1994, 371-394.
*}
+ options [document = false]
theories Confluence
session UNITY = ZF +
@@ -117,6 +131,7 @@
ZF/UNITY proofs.
*}
+ options [document = false]
theories
(*Simple examples: no composition*)
Mutex
@@ -134,6 +149,7 @@
Miscellaneous examples for Zermelo-Fraenkel Set Theory.
*}
+ options [document = false]
theories
misc
Ring (*abstract algebra*)
--- a/src/ZF/ZF.thy Tue Jul 24 12:36:59 2012 +0200
+++ b/src/ZF/ZF.thy Tue Jul 24 21:48:41 2012 +0200
@@ -6,7 +6,7 @@
header{*Zermelo-Fraenkel Set Theory*}
theory ZF
-imports FOL
+imports "~~/src/FOL/FOL"
begin
declare [[eta_contract = false]]