[isabelle-dev] New (Co)datatypes: Status & Plan 2
Makarius
makarius at sketis.net
Thu Nov 21 19:37:48 CET 2013
On Wed, 20 Nov 2013, Jasmin Blanchette wrote:
>> Can you say again which sessions/theories in which repository version
>> constitute the datatype vs. codatatype part?
>
> Version d983a020489d.
>
> The sessions "HOL-Cardinals-FP" and "HOL-BNF-FP" would be the things we need to move to HOL. They look like this:
>
> session "HOL-Cardinals-FP" in Cardinals = HOL +
> theories Cardinal_Arithmetic_FP
>
> session "HOL-BNF-FP" in BNF = "HOL-Cardinals-FP" +
> theories BNF_LFP BNF_GFP
>
> To compile the timing statistics I mentioned in my original email (e.g. 26 s for LFP + GFP), I ran (without building) the following session:
>
> session "HOL-BNF-FP" in BNF = HOL +
> theories BNF_LFP BNF_GFP
>
> with and without "BNF_GFP". Since then I've optimized the dependencies
> further -- the difference between LFP and GFP is now a couple of seconds
> only, and three theory files ("BNF_GFP.thy", "Equiv_Relations_More.thy",
> and "Sublist.thy") are needed by GFP only.
I have now done my own tests with the more recent version 2a3053472ec3
where the dependencies are simplified further.
The included changeset formalizes the experimental setup. In particular
sessions are defined like this:
session HOL1 = Pure +
theories Complex_Main "BNF/BNF_LFP"
session HOL2 = Pure +
theories Complex_Main "BNF/BNF_LFP" "BNF/BNF_GFP"
session "HOL1-Proofs" = Pure +
theories Proofs (*sequential change of global flag!*)
theories Main "BNF/BNF_LFP"
session "HOL2-Proofs" = Pure +
theories Proofs (*sequential change of global flag!*)
theories Main "BNF/BNF_LFP" "BNF/BNF_GFP"
The results on 8 cores * hyperthreading x86-darwin are as follows:
2 threads
Finished HOL (0:02:46 elapsed time, 0:04:56 cpu time, factor 1.78)
Finished HOL1 (0:02:55 elapsed time, 0:05:24 cpu time, factor 1.85)
Finished HOL2 (0:02:59 elapsed time, 0:05:29 cpu time, factor 1.83)
Finished HOL1-Proofs (0:05:40 elapsed time, 0:10:25 cpu time, factor 1.83)
Finished HOL2-Proofs (0:05:37 elapsed time, 0:10:41 cpu time, factor 1.90)
4 threads
Finished HOL (0:02:03 elapsed time, 0:05:08 cpu time, factor 2.50)
Finished HOL1 (0:02:11 elapsed time, 0:05:36 cpu time, factor 2.56)
Finished HOL2 (0:02:17 elapsed time, 0:06:00 cpu time, factor 2.62)
Finished HOL1-Proofs (0:03:26 elapsed time, 0:10:41 cpu time, factor 3.11)
Finished HOL2-Proofs (0:03:21 elapsed time, 0:11:02 cpu time, factor 3.29)
8 threads
Finished HOL (0:02:09 elapsed time, 0:05:11 cpu time, factor 2.41)
Finished HOL1 (0:01:59 elapsed time, 0:05:46 cpu time, factor 2.90)
Finished HOL2 (0:01:59 elapsed time, 0:05:52 cpu time, factor 2.95)
Finished HOL1-Proofs (0:02:47 elapsed time, 0:11:58 cpu time, factor 4.29)
Finished HOL2-Proofs (0:02:38 elapsed time, 0:12:21 cpu time, factor 4.68)
heaps
-r--r--r-- 1 makarius staff 168M 21 Nov 19:11 HOL
-r--r--r-- 1 makarius staff 177M 21 Nov 19:08 HOL1
-r--r--r-- 1 makarius staff 180M 21 Nov 19:05 HOL2
-r--r--r-- 1 makarius staff 198M 21 Nov 19:02 HOL1-Proofs
-r--r--r-- 1 makarius staff 201M 21 Nov 18:56 HOL2-Proofs
So the inclusion of GFP hardly matters concerning performance.
David Matthews did an excellent job in recent years to provide us enough
head-room in the HOL space to move on.
Note that I did *not* test SML/XL. It will take many hours in either
case, and is likely to be unhappy at first.
> Since codatatypes are spreading like a disease (with Andreas, Andrei,
> Dmitriy, and Johannes using them already) and are a central feature of
> other proof assistants, it would perhaps be nicer if we put them in
> "HOL" as well.
I would not call it a disease. I was first introduced to coinduction as a
"bottom-less pit" (Konrad Slind or some other guy from Camridge) in the
1990-ies. In that time people where still fond of continuous streams in
LCF.
Coinduction is a very useful tool in the standard toolbox, if it actually
does some practical work, and is not abused to show-off categorical
abstract non-sense. The HOL BNF project is a very positive example in
that respect.
Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1385057713 -3600
# Node ID 663262d367c603cf08bd304b909dafa1267357b6
# Parent 2a3053472ec334bc6c2118845a2b5e4e93ef9517
test;
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/BNF/BNF_FP_Base.thy
--- a/src/HOL/BNF/BNF_FP_Base.thy Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/BNF/BNF_FP_Base.thy Thu Nov 21 19:15:13 2013 +0100
@@ -10,7 +10,7 @@
header {* Shared Fixed Point Operations on Bounded Natural Functors *}
theory BNF_FP_Base
-imports BNF_Comp Ctr_Sugar
+imports BNF_Comp "../Ctr_Sugar"
begin
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/BNF/Equiv_Relations_More.thy
--- a/src/HOL/BNF/Equiv_Relations_More.thy Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/BNF/Equiv_Relations_More.thy Thu Nov 21 19:15:13 2013 +0100
@@ -8,7 +8,7 @@
header {* Some Preliminaries on Equivalence Relations and Quotients *}
theory Equiv_Relations_More
-imports Equiv_Relations Hilbert_Choice
+imports "../Equiv_Relations" "../Hilbert_Choice"
begin
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Thu Nov 21 19:15:13 2013 +0100
@@ -5,7 +5,7 @@
header {* Infinite Sets and Related Concepts *}
theory Infinite_Set
-imports Main
+imports "../Main"
begin
subsection "Infinite Sets"
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/Library/Order_Relation.thy Thu Nov 21 19:15:13 2013 +0100
@@ -3,7 +3,7 @@
header {* Orders as Relations *}
theory Order_Relation
-imports Main
+imports "../Main"
begin
subsection{* Orders on a set *}
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/Library/Wfrec.thy
--- a/src/HOL/Library/Wfrec.thy Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/Library/Wfrec.thy Thu Nov 21 19:15:13 2013 +0100
@@ -7,7 +7,7 @@
header {* Well-Founded Recursion Combinator *}
theory Wfrec
-imports Main
+imports "../Main"
begin
inductive
diff -r 2a3053472ec3 -r 663262d367c6 src/HOL/ROOT
--- a/src/HOL/ROOT Thu Nov 21 17:50:23 2013 +0100
+++ b/src/HOL/ROOT Thu Nov 21 19:15:13 2013 +0100
@@ -12,6 +12,20 @@
"document/root.bib"
"document/root.tex"
+session HOL1 = Pure +
+ theories Complex_Main "BNF/BNF_LFP"
+
+session HOL2 = Pure +
+ theories Complex_Main "BNF/BNF_LFP" "BNF/BNF_GFP"
+
+session "HOL1-Proofs" = Pure +
+ theories Proofs (*sequential change of global flag!*)
+ theories Main "BNF/BNF_LFP"
+
+session "HOL2-Proofs" = Pure +
+ theories Proofs (*sequential change of global flag!*)
+ theories Main "BNF/BNF_LFP" "BNF/BNF_GFP"
+
session "HOL-Proofs" = Pure +
description {*
HOL-Main with explicit proof terms.
-------------- next part --------------
"Pure" "Pure/Pure/Pure" "Pure" "" > ;
"Code_Generator" "HOL/HOL2/Code_Generator" "HOL2" + "Code_Generator.html" > "Pure/Pure/Pure" ;
"HOL" "HOL/HOL2/HOL" "HOL2" + "HOL.html" > "HOL/HOL2/Code_Generator" ;
"Orderings" "HOL/HOL2/Orderings" "HOL2" + "Orderings.html" > "HOL/HOL2/HOL" ;
"Groups" "HOL/HOL2/Groups" "HOL2" + "Groups.html" > "HOL/HOL2/Orderings" ;
"Lattices" "HOL/HOL2/Lattices" "HOL2" + "Lattices.html" > "HOL/HOL2/Groups" ;
"Set" "HOL/HOL2/Set" "HOL2" + "Set.html" > "HOL/HOL2/Lattices" ;
"Typedef" "HOL/HOL2/Typedef" "HOL2" + "Typedef.html" > "HOL/HOL2/Set" ;
"Complete_Lattices" "HOL/HOL2/Complete_Lattices" "HOL2" + "Complete_Lattices.html" > "HOL/HOL2/Set" ;
"Ctr_Sugar" "HOL/HOL2/Ctr_Sugar" "HOL2" + "Ctr_Sugar.html" > "HOL/HOL2/HOL" ;
"Inductive" "HOL/HOL2/Inductive" "HOL2" + "Inductive.html" > "HOL/HOL2/Complete_Lattices" "HOL/HOL2/Ctr_Sugar" ;
"Fun" "HOL/HOL2/Fun" "HOL2" + "Fun.html" > "HOL/HOL2/Complete_Lattices" ;
"Product_Type" "HOL/HOL2/Product_Type" "HOL2" + "Product_Type.html" > "HOL/HOL2/Typedef" "HOL/HOL2/Inductive" "HOL/HOL2/Fun" ;
"Sum_Type" "HOL/HOL2/Sum_Type" "HOL2" + "Sum_Type.html" > "HOL/HOL2/Typedef" "HOL/HOL2/Inductive" "HOL/HOL2/Fun" ;
"Rings" "HOL/HOL2/Rings" "HOL2" + "Rings.html" > "HOL/HOL2/Groups" ;
"Fields" "HOL/HOL2/Fields" "HOL2" + "Fields.html" > "HOL/HOL2/Rings" ;
"Nat" "HOL/HOL2/Nat" "HOL2" + "Nat.html" > "HOL/HOL2/Inductive" "HOL/HOL2/Typedef" "HOL/HOL2/Fun" "HOL/HOL2/Fields" ;
"Datatype" "HOL/HOL2/Datatype" "HOL2" + "Datatype.html" > "HOL/HOL2/Product_Type" "HOL/HOL2/Sum_Type" "HOL/HOL2/Nat" ;
"Option" "HOL/HOL2/Option" "HOL2" + "Option.html" > "HOL/HOL2/Datatype" ;
"Num" "HOL/HOL2/Num" "HOL2" + "Num.html" > "HOL/HOL2/Datatype" ;
"Power" "HOL/HOL2/Power" "HOL2" + "Power.html" > "HOL/HOL2/Num" ;
"Finite_Set" "HOL/HOL2/Finite_Set" "HOL2" + "Finite_Set.html" > "HOL/HOL2/Option" "HOL/HOL2/Power" ;
"Meson" "HOL/HOL2/Meson" "HOL2" + "Meson.html" > "HOL/HOL2/Datatype" ;
"ATP" "HOL/HOL2/ATP" "HOL2" + "ATP.html" > "HOL/HOL2/Meson" ;
"Metis" "HOL/HOL2/Metis" "HOL2" + "Metis.html" > "HOL/HOL2/ATP" ;
"Big_Operators" "HOL/HOL2/Big_Operators" "HOL2" + "Big_Operators.html" > "HOL/HOL2/Finite_Set" "HOL/HOL2/Metis" ;
"Relation" "HOL/HOL2/Relation" "HOL2" + "Relation.html" > "HOL/HOL2/Finite_Set" ;
"Equiv_Relations" "HOL/HOL2/Equiv_Relations" "HOL2" + "Equiv_Relations.html" > "HOL/HOL2/Big_Operators" "HOL/HOL2/Relation" ;
"Transitive_Closure" "HOL/HOL2/Transitive_Closure" "HOL2" + "Transitive_Closure.html" > "HOL/HOL2/Relation" ;
"Wellfounded" "HOL/HOL2/Wellfounded" "HOL2" + "Wellfounded.html" > "HOL/HOL2/Transitive_Closure" ;
"Hilbert_Choice" "HOL/HOL2/Hilbert_Choice" "HOL2" + "Hilbert_Choice.html" > "HOL/HOL2/Wellfounded" "HOL/HOL2/Big_Operators" ;
"Transfer" "HOL/HOL2/Transfer" "HOL2" + "Transfer.html" > "HOL/HOL2/Hilbert_Choice" ;
"Lifting" "HOL/HOL2/Lifting" "HOL2" + "Lifting.html" > "HOL/HOL2/Equiv_Relations" "HOL/HOL2/Transfer" ;
"Quotient" "HOL/HOL2/Quotient" "HOL2" + "Quotient.html" > "HOL/HOL2/Lifting" ;
"Complete_Partial_Order" "HOL/HOL2/Complete_Partial_Order" "HOL2" + "Complete_Partial_Order.html" > "HOL/HOL2/Product_Type" ;
"Partial_Function" "HOL/HOL2/Partial_Function" "HOL2" + "Partial_Function.html" > "HOL/HOL2/Complete_Partial_Order" "HOL/HOL2/Option" ;
"SAT" "HOL/HOL2/SAT" "HOL2" + "SAT.html" > "HOL/HOL2/HOL" ;
"FunDef" "HOL/HOL2/FunDef" "HOL2" + "FunDef.html" > "HOL/HOL2/Partial_Function" "HOL/HOL2/SAT" "HOL/HOL2/Wellfounded" ;
"Int" "HOL/HOL2/Int" "HOL2" + "Int.html" > "HOL/HOL2/Quotient" "HOL/HOL2/FunDef" ;
"Nat_Transfer" "HOL/HOL2/Nat_Transfer" "HOL2" + "Nat_Transfer.html" > "HOL/HOL2/Int" ;
"Divides" "HOL/HOL2/Divides" "HOL2" + "Divides.html" > "HOL/HOL2/Nat_Transfer" ;
"Code_Numeral" "HOL/HOL2/Code_Numeral" "HOL2" + "Code_Numeral.html" > "HOL/HOL2/Divides" ;
"Numeral_Simprocs" "HOL/HOL2/Numeral_Simprocs" "HOL2" + "Numeral_Simprocs.html" > "HOL/HOL2/Divides" ;
"Semiring_Normalization" "HOL/HOL2/Semiring_Normalization" "HOL2" + "Semiring_Normalization.html" > "HOL/HOL2/Numeral_Simprocs" ;
"Groebner_Basis" "HOL/HOL2/Groebner_Basis" "HOL2" + "Groebner_Basis.html" > "HOL/HOL2/Semiring_Normalization" ;
"Set_Interval" "HOL/HOL2/Set_Interval" "HOL2" + "Set_Interval.html" > "HOL/HOL2/Nat_Transfer" ;
"Presburger" "HOL/HOL2/Presburger" "HOL2" + "Presburger.html" > "HOL/HOL2/Groebner_Basis" "HOL/HOL2/Set_Interval" ;
"Lifting_Set" "HOL/HOL2/Lifting_Set" "HOL2" + "Lifting_Set.html" > "HOL/HOL2/Lifting" ;
"Lifting_Option" "HOL/HOL2/Lifting_Option" "HOL2" + "Lifting_Option.html" > "HOL/HOL2/Lifting" ;
"Lifting_Product" "HOL/HOL2/Lifting_Product" "HOL2" + "Lifting_Product.html" > "HOL/HOL2/Lifting" ;
"List" "HOL/HOL2/List" "HOL2" + "List.html" > "HOL/HOL2/Presburger" "HOL/HOL2/Code_Numeral" "HOL/HOL2/Lifting_Set" "HOL/HOL2/Lifting_Option" "HOL/HOL2/Lifting_Product" ;
"Random" "HOL/HOL2/Random" "HOL2" + "Random.html" > "HOL/HOL2/List" ;
"Map" "HOL/HOL2/Map" "HOL2" + "Map.html" > "HOL/HOL2/List" ;
"Enum" "HOL/HOL2/Enum" "HOL2" + "Enum.html" > "HOL/HOL2/Map" ;
"String" "HOL/HOL2/String" "HOL2" + "String.html" > "HOL/HOL2/Enum" ;
"Typerep" "HOL/HOL2/Typerep" "HOL2" + "Typerep.html" > "HOL/HOL2/String" ;
"Predicate" "HOL/HOL2/Predicate" "HOL2" + "Predicate.html" > "HOL/HOL2/String" ;
"Lazy_Sequence" "HOL/HOL2/Lazy_Sequence" "HOL2" + "Lazy_Sequence.html" > "HOL/HOL2/Predicate" ;
"Limited_Sequence" "HOL/HOL2/Limited_Sequence" "HOL2" + "Limited_Sequence.html" > "HOL/HOL2/Lazy_Sequence" ;
"Code_Evaluation" "HOL/HOL2/Code_Evaluation" "HOL2" + "Code_Evaluation.html" > "HOL/HOL2/Typerep" "HOL/HOL2/Limited_Sequence" ;
"Quickcheck_Random" "HOL/HOL2/Quickcheck_Random" "HOL2" + "Quickcheck_Random.html" > "HOL/HOL2/Random" "HOL/HOL2/Code_Evaluation" ;
"Random_Pred" "HOL/HOL2/Random_Pred" "HOL2" + "Random_Pred.html" > "HOL/HOL2/Quickcheck_Random" ;
"Random_Sequence" "HOL/HOL2/Random_Sequence" "HOL2" + "Random_Sequence.html" > "HOL/HOL2/Random_Pred" ;
"Quickcheck_Exhaustive" "HOL/HOL2/Quickcheck_Exhaustive" "HOL2" + "Quickcheck_Exhaustive.html" > "HOL/HOL2/Quickcheck_Random" ;
"Predicate_Compile" "HOL/HOL2/Predicate_Compile" "HOL2" + "Predicate_Compile.html" > "HOL/HOL2/Random_Sequence" "HOL/HOL2/Quickcheck_Exhaustive" ;
"Quickcheck_Narrowing" "HOL/HOL2/Quickcheck_Narrowing" "HOL2" + "Quickcheck_Narrowing.html" > "HOL/HOL2/Quickcheck_Exhaustive" ;
"Record" "HOL/HOL2/Record" "HOL2" + "Record.html" > "HOL/HOL2/Quickcheck_Narrowing" ;
"SMT" "HOL/HOL2/SMT" "HOL2" + "SMT.html" > "HOL/HOL2/Record" ;
"Sledgehammer" "HOL/HOL2/Sledgehammer" "HOL2" + "Sledgehammer.html" > "HOL/HOL2/SMT" ;
"Nitpick" "HOL/HOL2/Nitpick" "HOL2" + "Nitpick.html" > "HOL/HOL2/Sledgehammer" ;
"Extraction" "HOL/HOL2/Extraction" "HOL2" + "Extraction.html" > "HOL/HOL2/Option" ;
"Lifting_Sum" "HOL/HOL2/Lifting_Sum" "HOL2" + "Lifting_Sum.html" > "HOL/HOL2/Lifting" ;
"List_Prefix" "HOL/HOL2/List_Prefix" "HOL2" + "List_Prefix.html" > "HOL/HOL2/List" ;
"Coinduction" "HOL/HOL2/Coinduction" "HOL2" + "Coinduction.html" > "HOL/HOL2/Inductive" ;
"Main" "HOL/HOL2/Main" "HOL2" + "Main.html" > "HOL/HOL2/Predicate_Compile" "HOL/HOL2/Nitpick" "HOL/HOL2/Extraction" "HOL/HOL2/Lifting_Sum" "HOL/HOL2/List_Prefix" "HOL/HOL2/Coinduction" ;
"Fact" "HOL/HOL2/Fact" "HOL2" + "Fact.html" > "HOL/HOL2/Main" ;
"Parity" "HOL/HOL2/Parity" "HOL2" + "Parity.html" > "HOL/HOL2/Main" ;
"GCD" "HOL/HOL2/GCD" "HOL2" + "GCD.html" > "HOL/HOL2/Fact" "HOL/HOL2/Parity" ;
"Archimedean_Field" "HOL/HOL2/Archimedean_Field" "HOL2" + "Archimedean_Field.html" > "HOL/HOL2/Main" ;
"Rat" "HOL/HOL2/Rat" "HOL2" + "Rat.html" > "HOL/HOL2/GCD" "HOL/HOL2/Archimedean_Field" ;
"Conditionally_Complete_Lattices" "HOL/HOL2/Conditionally_Complete_Lattices" "HOL2" + "Conditionally_Complete_Lattices.html" > "HOL/HOL2/Main" ;
"Real" "HOL/HOL2/Real" "HOL2" + "Real.html" > "HOL/HOL2/Rat" "HOL/HOL2/Conditionally_Complete_Lattices" ;
"Topological_Spaces" "HOL/HOL2/Topological_Spaces" "HOL2" + "Topological_Spaces.html" > "HOL/HOL2/Conditionally_Complete_Lattices" ;
"Real_Vector_Spaces" "HOL/HOL2/Real_Vector_Spaces" "HOL2" + "Real_Vector_Spaces.html" > "HOL/HOL2/Real" "HOL/HOL2/Topological_Spaces" ;
"Limits" "HOL/HOL2/Limits" "HOL2" + "Limits.html" > "HOL/HOL2/Real_Vector_Spaces" ;
"Series" "HOL/HOL2/Series" "HOL2" + "Series.html" > "HOL/HOL2/Limits" ;
"Deriv" "HOL/HOL2/Deriv" "HOL2" + "Deriv.html" > "HOL/HOL2/Limits" ;
"NthRoot" "HOL/HOL2/NthRoot" "HOL2" + "NthRoot.html" > "HOL/HOL2/Deriv" ;
"Transcendental" "HOL/HOL2/Transcendental" "HOL2" + "Transcendental.html" > "HOL/HOL2/Series" "HOL/HOL2/NthRoot" ;
"Complex" "HOL/HOL2/Complex" "HOL2" + "Complex.html" > "HOL/HOL2/Transcendental" ;
"MacLaurin" "HOL/HOL2/MacLaurin" "HOL2" + "MacLaurin.html" > "HOL/HOL2/Transcendental" ;
"Taylor" "HOL/HOL2/Taylor" "HOL2" + "Taylor.html" > "HOL/HOL2/MacLaurin" ;
"Complex_Main" "HOL/HOL2/Complex_Main" "HOL2" + "Complex_Main.html" > "HOL/HOL2/Complex" "HOL/HOL2/Taylor" ;
"Order_Relation" "HOL/HOL2/Order_Relation" "HOL2" + "Order_Relation.html" > "HOL/HOL2/Main" ;
"Zorn" "HOL/HOL2/Zorn" "HOL2" + "Zorn.html" > "HOL/HOL2/Order_Relation" ;
"Infinite_Set" "HOL/HOL2/Infinite_Set" "HOL2" + "Infinite_Set.html" > "HOL/HOL2/Main" ;
"Fun_More_FP" "HOL/HOL2/Fun_More_FP" "HOL2" + "Fun_More_FP.html" > "HOL/HOL2/Infinite_Set" ;
"Order_Relation_More_FP" "HOL/HOL2/Order_Relation_More_FP" "HOL2" + "Order_Relation_More_FP.html" > "HOL/HOL2/Order_Relation" ;
"Wfrec" "HOL/HOL2/Wfrec" "HOL2" + "Wfrec.html" > "HOL/HOL2/Main" ;
"Wellfounded_More_FP" "HOL/HOL2/Wellfounded_More_FP" "HOL2" + "Wellfounded_More_FP.html" > "HOL/HOL2/Order_Relation_More_FP" "HOL/HOL2/Wfrec" ;
"Wellorder_Relation_FP" "HOL/HOL2/Wellorder_Relation_FP" "HOL2" + "Wellorder_Relation_FP.html" > "HOL/HOL2/Wellfounded_More_FP" ;
"Wellorder_Embedding_FP" "HOL/HOL2/Wellorder_Embedding_FP" "HOL2" + "Wellorder_Embedding_FP.html" > "HOL/HOL2/Zorn" "HOL/HOL2/Fun_More_FP" "HOL/HOL2/Wellorder_Relation_FP" ;
"Constructions_on_Wellorders_FP" "HOL/HOL2/Constructions_on_Wellorders_FP" "HOL2" + "Constructions_on_Wellorders_FP.html" > "HOL/HOL2/Wellorder_Embedding_FP" ;
"Cardinal_Order_Relation_FP" "HOL/HOL2/Cardinal_Order_Relation_FP" "HOL2" + "Cardinal_Order_Relation_FP.html" > "HOL/HOL2/Constructions_on_Wellorders_FP" ;
"Cardinal_Arithmetic_FP" "HOL/HOL2/Cardinal_Arithmetic_FP" "HOL2" + "Cardinal_Arithmetic_FP.html" > "HOL/HOL2/Cardinal_Order_Relation_FP" ;
"BNF_Util" "HOL/HOL2/BNF_Util" "HOL2" + "BNF_Util.html" > "HOL/HOL2/Cardinal_Arithmetic_FP" ;
"BNF_Def" "HOL/HOL2/BNF_Def" "HOL2" + "BNF_Def.html" > "HOL/HOL2/BNF_Util" ;
"Basic_BNFs" "HOL/HOL2/Basic_BNFs" "HOL2" + "Basic_BNFs.html" > "HOL/HOL2/BNF_Def" ;
"BNF_Comp" "HOL/HOL2/BNF_Comp" "HOL2" + "BNF_Comp.html" > "HOL/HOL2/Basic_BNFs" ;
"BNF_FP_Base" "HOL/HOL2/BNF_FP_Base" "HOL2" + "BNF_FP_Base.html" > "HOL/HOL2/BNF_Comp" ;
"BNF_LFP" "HOL/HOL2/BNF_LFP" "HOL2" + "BNF_LFP.html" > "HOL/HOL2/BNF_FP_Base" ;
"Equiv_Relations_More" "HOL/HOL2/Equiv_Relations_More" "HOL2" + "Equiv_Relations_More.html" > "HOL/HOL2/Equiv_Relations" "HOL/HOL2/Hilbert_Choice" ;
"BNF_GFP" "HOL/HOL2/BNF_GFP" "HOL2" + "BNF_GFP.html" > "HOL/HOL2/BNF_FP_Base" "HOL/HOL2/Equiv_Relations_More" ;
More information about the isabelle-dev
mailing list