Commit d99b58cf authored by haftmann's avatar haftmann
Browse files

tuned theory structure

parent c272e0d255f2
(*<*)
theory Blue_Eyes
imports Main
imports
"HOL-Combinatorics.Transposition"
begin
(*>*)
......
chapter AFP
session Blue_Eyes (AFP) = HOL +
session Blue_Eyes (AFP) = "HOL-Combinatorics" +
options [timeout = 300]
theories
Blue_Eyes
......
......@@ -3,7 +3,8 @@
*)
section \<open>Gauss-Jordan elimination algorithm\<close>
theory Gauss_Jordan_Elim_Fun
imports Main
imports
"HOL-Combinatorics.Transposition"
begin
text\<open>Matrices are functions:\<close>
......
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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment