diff --git a/thys/Blue_Eyes/Blue_Eyes.thy b/thys/Blue_Eyes/Blue_Eyes.thy --- a/thys/Blue_Eyes/Blue_Eyes.thy +++ b/thys/Blue_Eyes/Blue_Eyes.thy @@ -1,424 +1,425 @@ (*<*) theory Blue_Eyes - imports Main + imports + "HOL-Combinatorics.Transposition" begin (*>*) section \Introduction\ text \The original problem statement @{cite xkcd} explains the puzzle well: \begin{quotation} A group of people with assorted eye colors live on an island. They are all perfect logicians -- if a conclusion can be logically deduced, they will do it instantly. No one knows the color of their eyes. Every night at midnight, a ferry stops at the island. Any islanders who have figured out the color of their own eyes then leave the island, and the rest stay. Everyone can see everyone else at all times and keeps a count of the number of people they see with each eye color (excluding themselves), but they cannot otherwise communicate. Everyone on the island knows all the rules in this paragraph. On this island there are 100 blue-eyed people, 100 brown-eyed people, and the Guru (she happens to have green eyes). So any given blue-eyed person can see 100 people with brown eyes and 99 people with blue eyes (and one with green), but that does not tell him his own eye color; as far as he knows the totals could be 101 brown and 99 blue. Or 100 brown, 99 blue, and he could have red eyes. The Guru is allowed to speak once (let's say at noon), on one day in all their endless years on the island. Standing before the islanders, she says the following: I can see someone who has blue eyes.'' Who leaves the island, and on what night? \end{quotation} It might seem weird that the Guru's declaration gives anyone any new information. For an informal discussion, see \cite[Section~1.1]{fagin1995}.\ section \Modeling the world \label{sec:world}\ text \We begin by fixing two type variables: @{typ "'color"} and @{typ "'person"}. The puzzle doesn't specify how many eye colors are possible, but four are mentioned. Crucially, we must assume they are distinct. We specify the existence of colors other than blue and brown, even though we don't mention them later, because when blue and brown are the only possible colors, the puzzle has a different solution — the brown-eyed logicians may leave one day after the blue-eyed ones. We refrain from specifying the exact population of the island, choosing to only assume it is finite and denote a specific person as the Guru. We could also model the Guru as an outside entity instead of a participant. This doesn't change the answer and results in a slightly simpler proof, but is less faithful to the problem statement.\ context fixes blue brown green red :: 'color assumes colors_distinct: "distinct [blue, brown, green, red]" fixes guru :: 'person assumes "finite (UNIV :: 'person set)" begin text \It's slightly tricky to formalize the behavior of perfect logicians. The representation we use is centered around the type of a @{emph \world\}, which describes the entire state of the environment. In our case, it's a function @{typ "'person => 'color"} that assigns an eye color to everyone.@{footnote \We would introduce a type synonym, but at the time of writing Isabelle doesn't support including type variables fixed by a locale in a type synonym.\} The only condition known to everyone and not dependent on the observer is Guru's declaration:\ definition valid :: "('person \ 'color) \ bool" where "valid w \ (\p. p \ guru \ w p = blue)" text \We then define the function @{term "possible n p w w'"}, which returns @{term True} if on day \n\ the potential world \w'\ is plausible from the perspective of person \p\, based on the observations they made in the actual world \w\. Then, @{term "leaves n p w"} is @{term True} if \p\ is able to unambiguously deduce the color of their own eyes, i.e. if it is the same in all possible worlds. Note that if \p\ actually left many moons ago, this function still returns @{term True}.\ fun leaves :: "nat \ 'person \ ('person \ 'color) \ bool" and possible :: "nat \ 'person \ ('person \ 'color) \ ('person \ 'color) \ bool" where "leaves n p w = (\w'. possible n p w w' \ w' p = w p)" | "possible n p w w' \ valid w \ valid w' \ (\p' \ p. w p' = w' p') \ (\n' < n. \p'. leaves n' p' w = leaves n' p' w')" text \Naturally, the act of someone leaving can be observed by others, thus the two definitions are mutually recursive. As such, we need to instruct the simplifier to not unfold these definitions endlessly.\ declare possible.simps[simp del] leaves.simps[simp del] text \A world is possible if \<^enum> The Guru's declaration holds. \<^enum> The eye color of everyone but the observer matches. \<^enum> The same people left on each of the previous days. Moreover, we require that the actual world \w\ is \valid\, so that the relation is symmetric:\ lemma possible_sym: "possible n p w w' = possible n p w' w" by (auto simp: possible.simps) text \In fact, \possible n p\ is an equivalence relation:\ lemma possible_refl: "valid w \ possible n p w w" by (auto simp: possible.simps) lemma possible_trans: "possible n p w1 w2 \ possible n p w2 w3 \ possible n p w1 w3" by (auto simp: possible.simps) section \Eye colors other than blue\ text \Since there is no way to distinguish between the colors other than blue, only the blue-eyed people will ever leave. To formalize this notion, we define a function that takes a world and replaces the eye color of a specified person. The original color is specified too, so that the transformation composes nicely with the recursive hypothetical worlds of @{const possible}.\ definition try_swap :: "'person \ 'color \ 'color \ ('person \ 'color) \ ('person \ 'color)" where "try_swap p c\<^sub>1 c\<^sub>2 w x = (if c\<^sub>1 = blue \ c\<^sub>2 = blue \ x \ p then w x else Fun.swap c\<^sub>1 c\<^sub>2 id (w x))" lemma try_swap_valid[simp]: "valid (try_swap p c\<^sub>1 c\<^sub>2 w) = valid w" by (auto simp add: try_swap_def valid_def swap_id_eq) lemma try_swap_eq[simp]: "try_swap p c\<^sub>1 c\<^sub>2 w x = try_swap p c\<^sub>1 c\<^sub>2 w' x \ w x = w' x" by (auto simp add: try_swap_def swap_id_eq) lemma try_swap_inv[simp]: "try_swap p c\<^sub>1 c\<^sub>2 (try_swap p c\<^sub>1 c\<^sub>2 w) = w" by (rule ext) (auto simp add: try_swap_def swap_id_eq) lemma leaves_try_swap[simp]: assumes "valid w" shows "leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w) = leaves n p w" using assms proof (induction n arbitrary: p w rule: less_induct) case (less n) have "leaves n p w" if "leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w)" for w proof (unfold leaves.simps; rule+) fix w' assume "possible n p w w'" then have "possible n p (try_swap p' c\<^sub>1 c\<^sub>2 w) (try_swap p' c\<^sub>1 c\<^sub>2 w')" by (fastforce simp: possible.simps less.IH) with leaves n p (try_swap p' c\<^sub>1 c\<^sub>2 w) have "try_swap p' c\<^sub>1 c\<^sub>2 w' p = try_swap p' c\<^sub>1 c\<^sub>2 w p" unfolding leaves.simps by simp thus "w' p = w p" by simp qed with try_swap_inv show ?case by auto qed text \This lets us prove that only blue-eyed people will ever leave the island.\ proposition only_blue_eyes_leave: assumes "leaves n p w" and "valid w" shows "w p = blue" proof (rule ccontr) assume "w p \ blue" then obtain c where c: "w p \ c" "c \ blue" using colors_distinct by (metis distinct_length_2_or_more) let ?w' = "try_swap p (w p) c w" have "possible n p w ?w'" using valid w apply (simp add: possible.simps) by (auto simp: try_swap_def) moreover have "?w' p \ w p" using c w p \ blue by (auto simp: try_swap_def) ultimately have "\ leaves n p w" by (auto simp: leaves.simps) with assms show False by simp qed section "The blue-eyed logicians" text \We will now consider the behavior of the logicians with blue eyes. First, some simple lemmas. Reasoning about set cardinalities often requires considering infinite sets separately. Usefully, all sets of people are finite by assumption.\ lemma people_finite[simp]: "finite (S::'person set)" proof (rule finite_subset) show "S \ UNIV" by auto show "finite (UNIV::'person set)" by fact qed text \Secondly, we prove a destruction rule for @{const possible}. It is strictly weaker than the definition, but thanks to the simpler form, it's easier to guide the automation with it.\ lemma possibleD_colors: assumes "possible n p w w'" and "p' \ p" shows "w' p' = w p'" using assms unfolding possible.simps by simp text \A central concept in the reasoning is the set of blue-eyed people someone can see.\ definition blues_seen :: "('person \ 'color) \ 'person \ 'person set" where "blues_seen w p = {p'. w p' = blue} - {p}" lemma blues_seen_others: assumes "w p' = blue" and "p \ p'" shows "w p = blue \ card (blues_seen w p) = card (blues_seen w p')" and "w p \ blue \ card (blues_seen w p) = Suc (card (blues_seen w p'))" proof - assume "w p = blue" then have "blues_seen w p' = blues_seen w p \ {p} - {p'}" by (auto simp add: blues_seen_def) moreover have "p \ blues_seen w p" unfolding blues_seen_def by auto moreover have "p' \ blues_seen w p \ {p}" unfolding blues_seen_def using p \ p' w p' = blue by auto ultimately show "card (blues_seen w p) = card (blues_seen w p')" by simp next assume "w p \ blue" then have "blues_seen w p' = blues_seen w p - {p'}" by (auto simp add: blues_seen_def) moreover have "p' \ blues_seen w p" unfolding blues_seen_def using p \ p' w p' = blue by auto ultimately show "card (blues_seen w p) = Suc (card (blues_seen w p'))" by (simp only: card_Suc_Diff1 people_finite) qed lemma blues_seen_same[simp]: assumes "possible n p w w'" shows "blues_seen w' p = blues_seen w p" using assms by (auto simp: blues_seen_def possible.simps) lemma possible_blues_seen: assumes "possible n p w w'" assumes "w p' = blue" and "p \ p'" shows "w' p = blue \ card (blues_seen w p) = card (blues_seen w' p')" and "w' p \ blue \ card (blues_seen w p) = Suc (card (blues_seen w' p'))" using possibleD_colors[OF possible n p w w'] and blues_seen_others assms by (auto simp flip: blues_seen_same) text \Finally, the crux of the solution. We proceed by strong induction.\ lemma blue_leaves: assumes "w p = blue" and "valid w" and guru: "w guru \ blue" shows "leaves n p w \ n \ card (blues_seen w p)" using assms proof (induction n arbitrary: p w rule: less_induct) case (less n) show ?case proof \ \First, we show that day \n\ is sufficient to deduce that the eyes are blue.\ assume "n \ card (blues_seen w p)" have "w' p = blue" if "possible n p w w'" for w' proof (cases "card (blues_seen w' p)") case 0 moreover from possible n p w w' have "valid w'" by (simp add: possible.simps) ultimately show "w' p = blue" unfolding valid_def blues_seen_def by auto next case (Suc k) \ \We consider the behavior of somebody else, who also has blue eyes.\ then have "blues_seen w' p \ {}" by auto then obtain p' where "w' p' = blue" and "p \ p'" unfolding blues_seen_def by auto then have "w p' = blue" using possibleD_colors[OF possible n p w w'] by simp have "p \ guru" using w p = blue and w guru \ blue by auto hence "w' guru \ blue" using w guru \ blue and possibleD_colors[OF possible n p w w'] by simp have "valid w'" using possible n p w w' unfolding possible.simps by simp show "w' p = blue" proof (rule ccontr) assume "w' p \ blue" \ \If our eyes weren't blue, then \p'\ would see one blue-eyed person less than us.\ with possible_blues_seen[OF possible n p w w' w p' = blue p \ p'] have *: "card (blues_seen w p) = Suc (card (blues_seen w' p'))" by simp \ \By induction, they would've left on day \k = blues_seen w' p'\.\ let ?k = "card (blues_seen w' p')" have "?k < n" using n \ card (blues_seen w p) and * by simp hence "leaves ?k p' w'" using valid w' w' p' = blue w' guru \ blue by (intro less.IH[THEN iffD2]; auto) \ \However, we know that actually, \p'\ didn't leave that day yet.\ moreover have "\ leaves ?k p' w" proof assume "leaves ?k p' w" then have "?k \ card (blues_seen w p')" using ?k < n w p' = blue valid w w guru \ blue by (intro less.IH[THEN iffD1]; auto) have "card (blues_seen w p) = card (blues_seen w p')" by (intro blues_seen_others; fact) with * have "?k < card (blues_seen w p')" by simp with ?k \ card (blues_seen w p') show False by simp qed moreover have "leaves ?k p' w' = leaves ?k p' w" using possible n p w w' ?k < n unfolding possible.simps by simp ultimately show False by simp qed qed thus "leaves n p w" unfolding leaves.simps using w p = blue by simp next \ \Then, we show that it's not possible to deduce the eye color any earlier.\ { assume "n < card (blues_seen w p)" \ \Consider a hypothetical world where \p\ has brown eyes instead. We will prove that this world is \possible\.\ let ?w' = "w(p := brown)" have "?w' guru \ blue" using w guru \ blue w p = blue by auto have "valid ?w'" proof - from n < card (blues_seen w p) have "card (blues_seen w p) \ 0" by auto hence "blues_seen w p \ {}" by auto then obtain p' where "p' \ blues_seen w p" by auto hence "p \ p'" and "w p' = blue" by (auto simp: blues_seen_def) hence "?w' p' = blue" by auto with ?w' guru \ blue show "valid ?w'" unfolding valid_def by auto qed moreover have "leaves n' p' w = leaves n' p' ?w'" if "n' < n" for n' p' proof - have not_leavesI: "\leaves n' p' w'" if "valid w'" "w' guru \ blue" and P: "w' p' = blue \ n' < card (blues_seen w' p')" for w' proof (cases "w' p' = blue") case True then have "leaves n' p' w' \ n' \ card (blues_seen w' p')" using less.IH n' < n valid w' w' guru \ blue by simp with P[OF w' p' = blue] show "\leaves n' p' w'" by simp next case False then show "\ leaves n' p' w'" using only_blue_eyes_leave valid w' by auto qed have "\leaves n' p' w" proof (intro not_leavesI) assume "w p' = blue" with w p = blue have "card (blues_seen w p) = card (blues_seen w p')" apply (cases "p = p'", simp) by (intro blues_seen_others; auto) with n' < n and n < card (blues_seen w p) show "n' < card (blues_seen w p')" by simp qed fact+ moreover have "\ leaves n' p' ?w'" proof (intro not_leavesI) assume "?w' p' = blue" with colors_distinct have "p \ p'" and "?w' p \ blue" by auto hence "card (blues_seen ?w' p) = Suc (card (blues_seen ?w' p'))" using ?w' p' = blue by (intro blues_seen_others; auto) moreover have "blues_seen w p = blues_seen ?w' p" unfolding blues_seen_def by auto ultimately show "n' < card (blues_seen ?w' p')" using n' < n and n < card (blues_seen w p) by auto qed fact+ ultimately show "leaves n' p' w = leaves n' p' ?w'" by simp qed ultimately have "possible n p w ?w'" using valid w by (auto simp: possible.simps) moreover have "?w' p \ blue" using colors_distinct by auto ultimately have "\ leaves n p w" unfolding leaves.simps using w p = blue by blast } then show "leaves n p w \ n \ card (blues_seen w p)" by fastforce qed qed text \This can be combined into a theorem that describes the behavior of the logicians based on the objective count of blue-eyed people, and not the count by a specific person. The xkcd puzzle is the instance where \n = 99\.\ theorem blue_eyes: assumes "card {p. w p = blue} = Suc n" and "valid w" and "w guru \ blue" shows "leaves k p w \ w p = blue \ k \ n" proof (cases "w p = blue") case True with assms have "card (blues_seen w p) = n" unfolding blues_seen_def by simp then show ?thesis using w p = blue valid w w guru \ blue blue_leaves by simp next case False then show ?thesis using only_blue_eyes_leave valid w by auto qed end (*<*) end (*>*) section \Future work\ text \After completing this formalization, I have been made aware of epistemic logic. The @{emph \possible worlds\} model in \cref{sec:world} turns out to be quite similar to the usual semantics of this logic. It might be interesting to solve this puzzle within the axiom system of epistemic logic, without explicit reasoning about possible worlds.\ \ No newline at end of file diff --git a/thys/Blue_Eyes/ROOT b/thys/Blue_Eyes/ROOT --- a/thys/Blue_Eyes/ROOT +++ b/thys/Blue_Eyes/ROOT @@ -1,9 +1,9 @@ chapter AFP -session Blue_Eyes (AFP) = HOL + +session Blue_Eyes (AFP) = "HOL-Combinatorics" + options [timeout = 300] theories Blue_Eyes document_files "root.tex" "root.bib" diff --git a/thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy b/thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy --- a/thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy +++ b/thys/Gauss-Jordan-Elim-Fun/Gauss_Jordan_Elim_Fun.thy @@ -1,261 +1,262 @@ (* Gauss-Jordan elimination for matrices represented as functions Author: Tobias Nipkow *) section \Gauss-Jordan elimination algorithm\ theory Gauss_Jordan_Elim_Fun -imports Main + imports + "HOL-Combinatorics.Transposition" begin text\Matrices are functions:\ type_synonym 'a matrix = "nat \ nat \ 'a" text\In order to restrict to finite matrices, a matrix is usually combined with one or two natural numbers indicating the maximal row and column of the matrix. Gauss-Jordan elimination is parameterized with a natural number \n\. It indicates that the matrix \A\ has \n\ rows and columns. In fact, \A\ is the augmented matrix with \n+1\ columns. Column \n\ is the right-hand side'', i.e.\ the constant vector \b\. The result is the unit matrix augmented with the solution in column \n\; see the correctness theorem below.\ fun gauss_jordan :: "('a::field)matrix \ nat \ ('a)matrix option" where "gauss_jordan A 0 = Some(A)" | "gauss_jordan A (Suc m) = (case dropWhile (\i. A i m = 0) [0.. None | p # _ \ (let Ap' = (\j. A p j / A p m); A' = (\i. if i=p then Ap' else (\j. A i j - A i m * Ap' j)) in gauss_jordan (Fun.swap p m A') m))" text\Some auxiliary functions:\ definition solution :: "('a::field)matrix \ nat \ (nat \ 'a) \ bool" where "solution A n x = (\i j=0.. nat \ nat \ bool" where "unit A m n = (\i j::nat. m\j \ j A i j = (if i=j then 1 else 0))" lemma solution_swap: assumes "p1 < n" "p2 < n" shows "solution (Fun.swap p1 p2 A) n x = solution A n x" (is "?L = ?R") proof(cases "p1=p2") case True thus ?thesis by simp next case False show ?thesis proof assume ?R thus ?L using assms False by(simp add: solution_def Fun.swap_def) next assume ?L show ?R proof(auto simp: solution_def) fix i assume "ij = 0..?L\ assms False show ?thesis by(fastforce simp add: solution_def Fun.swap_def) next assume "i\p1" show ?thesis proof cases assume "i=p2" with \?L\ assms False show ?thesis by(fastforce simp add: solution_def Fun.swap_def) next assume "i\p2" with \i\p1\ \?L\ \i assms False show ?thesis by(fastforce simp add: solution_def Fun.swap_def) qed qed qed qed qed (* Converting these apply scripts makes them blow up - see above *) lemma solution_upd1: "c \ 0 \ solution (A(p:=(\j. A p j / c))) n x = solution A n x" apply(cases "p ap = A p; \i j. i\p \ a i j = A i j; p \ solution (\i. if i=p then ap else (\j. a i j - c i * ap j)) n x = solution A n x" apply(clarsimp simp add: solution_def) apply rule prefer 2 apply (simp add: field_simps sum_subtractf sum_distrib_left[symmetric]) apply(clarsimp) apply(case_tac "i=p") apply simp apply (auto simp add: field_simps sum_subtractf sum_distrib_left[symmetric] all_conj_distrib) done subsection\Correctness\ text\The correctness proof:\ lemma gauss_jordan_lemma: "m\n \ unit A m n \ gauss_jordan A m = Some B \ unit B 0 n \ solution A n (\j. B j n)" proof(induct m arbitrary: A B) case 0 { fix a and b c d :: "'a" have "(if a then b else c) * d = (if a then b*d else c*d)" by simp } with 0 show ?case by(simp add: unit_def solution_def sum.If_cases) next case (Suc m) let "?Ap' p" = "(\j. A p j / A p m)" let "?A' p" = "(\i. if i=p then ?Ap' p else (\j. A i j - A i m * ?Ap' p j))" from \gauss_jordan A (Suc m) = Some B\ obtain p ks where "dropWhile (\i. A i m = 0) [0..m" "A p m \ 0" apply(simp_all add: dropWhile_eq_Cons_conv del:upt_Suc) by (metis set_upt atLeast0AtMost atLeastLessThanSuc_atLeastAtMost atMost_iff in_set_conv_decomp) have "m\n" "mSuc m \ n\ by arith+ have "unit (Fun.swap p m (?A' p)) m n" using Suc.prems(2) p unfolding unit_def Fun.swap_def Suc_le_eq by (auto simp: le_less) from Suc.hyps[OF \m\n\ this rec] \m p show ?case by(simp add: solution_swap solution_upd1 solution_upd_but1[where A = "A(p := ?Ap' p)"]) qed theorem gauss_jordan_correct: "gauss_jordan A n = Some B \ solution A n (\j. B j n)" by(simp add:gauss_jordan_lemma[of n n] unit_def field_simps) definition solution2 :: "('a::field)matrix \ nat \ nat \ (nat \ 'a) \ bool" where "solution2 A m n x = (\i j=0.. solution2 A m n x \ (\y. solution2 A m n y \ (\jp 0" proof(rule ccontr) assume "\(\p 0)" hence 1: "\p. p A p q = 0" by simp { fix y assume 2: "\j. j\q \ y j = x j" { fix i assume "ij = 0..i] 2 have "(\j = 0..q < m\ show False by (simp add: usolution_def) (metis fun_upd_same zero_neq_one) qed lemma lem1: fixes f :: "'a \ 'b::field" shows "(\x\A. f x * (a * g x)) = a * (\x\A. f x * g x)" by (simp add: sum_distrib_left field_simps) lemma lem2: fixes f :: "'a \ 'b::field" shows "(\x\A. f x * (g x * a)) = a * (\x\A. f x * g x)" by (simp add: sum_distrib_left field_simps) subsection\Complete\ lemma gauss_jordan_complete: "m \ n \ usolution A m n x \ \B. gauss_jordan A m = Some B" proof(induction m arbitrary: A) case 0 show ?case by simp next case (Suc m A) from \Suc m \ n\ have "m\n" and "mm] obtain p' where "p' 0" by blast hence "dropWhile (\i. A i m = 0) [0.. []" by (simp add: atLeast0LessThan) (metis lessThan_iff linorder_neqE_nat not_less_eq) then obtain p xs where 1: "dropWhile (\i. A i m = 0) [0..m" "A p m \ 0" by (simp_all add: dropWhile_eq_Cons_conv del: upt_Suc) (metis set_upt atLeast0AtMost atLeastLessThanSuc_atLeastAtMost atMost_iff in_set_conv_decomp) then have p: "p < Suc m" "A p m \ 0" by auto let ?Ap' = "(\j. A p j / A p m)" let ?A' = "(\i. if i=p then ?Ap' else (\j. A i j - A i m * ?Ap' j))" let ?A = "Fun.swap p m ?A'" have A: "solution2 A (Suc m) n x" using Suc.prems(2) by(simp add: usolution_def) { fix i assume le_m: "p < Suc m" "i < Suc m" "A p m \ 0" have "(\j = 0..j = 0..j = 0.. = A i n - A p n * A i m / A p m" using A le_m by (simp add: solution2_def field_simps del: sum.op_ivl_Suc) finally have "(\j = 0..j=0.. p" show ?thesis proof (cases "i = m") assume "i = m" with p \i \ p\ have "p < m" by simp with a[unfolded solution2_def, THEN spec, of p] p(2) have "A p m * (A m m * A p n + A p m * (\j = 0..j = 0..A p m \ 0\ show ?thesis unfolding \i = m\ by simp (simp add: field_simps) next assume "i \ m" then have "i < m" using \i < Suc m\ by simp with a[unfolded solution2_def, THEN spec, of i] p(2) have "A p m * (A i m * A p n + A p m * (\j = 0..j = 0..A p m \ 0\ show ?thesis by simp (simp add: field_simps) qed qed qed with \usolution A (Suc m) n x\ have "\jjm\n\ this] 1 show ?case by(simp) qed text\Future work: extend the proof to matrix inversion.\ hide_const (open) unit end diff --git a/thys/Gauss-Jordan-Elim-Fun/ROOT b/thys/Gauss-Jordan-Elim-Fun/ROOT --- a/thys/Gauss-Jordan-Elim-Fun/ROOT +++ b/thys/Gauss-Jordan-Elim-Fun/ROOT @@ -1,8 +1,8 @@ chapter AFP -session "Gauss-Jordan-Elim-Fun" (AFP) = HOL + +session "Gauss-Jordan-Elim-Fun" (AFP) = "HOL-Combinatorics" + options [timeout = 600] theories Gauss_Jordan_Elim_Fun document_files "root.tex"