summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/ROOT

changeset 48975 | 7f79f94a432c |

parent 48932 | c6e679443adc |

child 48976 | 2d17c305f4bc |

--- a/src/HOL/ROOT Tue Aug 28 16:33:06 2012 +0200 +++ b/src/HOL/ROOT Tue Aug 28 17:16:00 2012 +0200 @@ -597,6 +597,37 @@ theories Nominal_Examples theories [quick_and_dirty] VC_Condition +session "HOL-Ordinals_and_Cardinals-Base" in Ordinals_and_Cardinals = HOL + + options [document = false] + theories Cardinal_Arithmetic + +session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals = + "HOL-Ordinals_and_Cardinals-Base" + + options [document = false] + theories Cardinal_Order_Relation + +session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" + + options [document = false] + theories Codatatype + +session "HOL-Codatatype-Examples" in "Codatatype/Examples" = "HOL-Codatatype" + + options [document = false] + theories + HFset + Lambda_Term + Process + TreeFsetI + (* FIXME: shouldn't require "parallel_proofs = 0"; + with parallel proofs enabled, the build of this session + takes 10 times longer *) + theories [parallel_proofs = 0] + "Infinite_Derivation_Trees/Gram_Lang" + "Infinite_Derivation_Trees/Parallel" + Stream + theories [parallel_proofs = 0, condition = ISABELLE_FULL_TEST] + Misc_Codata + Misc_Data + session "HOL-Word" in Word = HOL + options [document_graph] theories Word