Loading theory "Pell.Efficient_Discrete_Sqrt"
Loading theory "Pell.Pell"
locale pell
  fixes D :: "nat"
  assumes "pell D"
### theory "Pell.Pell"
### 0.746s elapsed time, 1.532s cpu time, 0.000s GC time
*** Undefined fact: "pow_divs_eq" (line 63 of "~~/afp/thys/Pell/Pell.thy")
*** At command "by" (line 63 of "~~/afp/thys/Pell/Pell.thy")
Found termination order: "(\<lambda>p. size (fst p)) <*mlex*> {}"
### theory "Pell.Efficient_Discrete_Sqrt"
### 1.956s elapsed time, 3.504s cpu time, 0.000s GC time
Loading theory "Pell.Pell_Algorithm"
Found termination order: "{}"
### theory "Pell.Pell_Algorithm"
### 1.452s elapsed time, 2.860s cpu time, 0.160s GC time
Loading theory "Pell.Pell_Algorithm_Test"
### theory "Pell.Pell_Algorithm_Test"
### 0.303s elapsed time, 0.604s cpu time, 0.000s GC time
*** Undefined fact: "pow_divs_eq" (line 63 of "~~/afp/thys/Pell/Pell.thy")
*** At command "by" (line 63 of "~~/afp/thys/Pell/Pell.thy")