Path	Lines of Code
isabelle/valid/aimeII_2020_p6.thy	14
isabelle/valid/aimeI_2000_p7.thy	19
isabelle/valid/aimeI_2001_p3.thy	16
isabelle/valid/aime_1983_p9.thy	24
isabelle/valid/aime_1984_p15.thy	18
isabelle/valid/aime_1984_p5.thy	12
isabelle/valid/aime_1987_p8.thy	13
isabelle/valid/aime_1988_p3.thy	13
isabelle/valid/aime_1988_p4.thy	14
isabelle/valid/aime_1990_p2.thy	11
isabelle/valid/aime_1991_p1.thy	14
isabelle/valid/aime_1991_p6.thy	13
isabelle/valid/aime_1994_p4.thy	13
isabelle/valid/aime_1996_p5.thy	20
isabelle/valid/aime_1997_p12.thy	12
isabelle/valid/algebra_2complexrootspoly_xsqp49eqxp7itxpn7i.thy	11
isabelle/valid/algebra_2rootsintpoly_am10tap11eqasqpam110.thy	19
isabelle/valid/algebra_2rootspoly_apatapbeq2asqp2ab.thy	11
isabelle/valid/algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4.thy	18
isabelle/valid/algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta.thy	11
isabelle/valid/algebra_amgm_faxinrrp2msqrt2geq2mxm1div2x.thy	10
isabelle/valid/algebra_amgm_prod1toneq1_sum1tongeqn.thy	14
isabelle/valid/algebra_amgm_sqrtxymulxmyeqxpy_xpygeq4.thy	14
isabelle/valid/algebra_amgm_sumasqdivbsqgeqsumbdiva.thy	12
isabelle/valid/algebra_apb4leq8ta4pb4.thy	12
isabelle/valid/algebra_binomnegdiscrineq_10alt28asqp1.thy	11
isabelle/valid/algebra_manipexpr_2erprsqpesqeqnrpnesq.thy	11
isabelle/valid/algebra_manipexpr_apbeq2cceqiacpbceqm2.thy	13
isabelle/valid/algebra_sqineq_2at2pclta2c2p41pc.thy	11
isabelle/valid/algebra_sqineq_2unitcircatblt1.thy	24
isabelle/valid/algebra_sqineq_36azm9asqle36zsq.thy	11
isabelle/valid/algebra_sqineq_4bap1lt4bsqpap1sq.thy	11
isabelle/valid/algebra_xmysqpymzsqpzmxsqeqxyz_xpypzp6dvdx3y3z3.thy	12
isabelle/valid/amc12_2000_p11.thy	14
isabelle/valid/amc12_2000_p15.thy	14
isabelle/valid/amc12_2000_p5.thy	12
isabelle/valid/amc12_2001_p2.thy	15
isabelle/valid/amc12_2001_p9.thy	20
isabelle/valid/amc12a_2002_p1.thy	14
isabelle/valid/amc12a_2002_p12.thy	15
isabelle/valid/amc12a_2002_p21.thy	15
isabelle/valid/amc12a_2003_p1.thy	23
isabelle/valid/amc12a_2003_p24.thy	35
isabelle/valid/amc12a_2003_p25.thy	14
isabelle/valid/amc12a_2008_p15.thy	12
isabelle/valid/amc12a_2008_p2.thy	16
isabelle/valid/amc12a_2008_p4.thy	10
isabelle/valid/amc12a_2008_p8.thy	19
isabelle/valid/amc12a_2009_p15.thy	14
isabelle/valid/amc12a_2009_p2.thy	10
isabelle/valid/amc12a_2009_p25.thy	14
isabelle/valid/amc12a_2009_p5.thy	22
isabelle/valid/amc12a_2009_p9.thy	14
isabelle/valid/amc12a_2010_p10.thy	17
isabelle/valid/amc12a_2010_p11.thy	14
isabelle/valid/amc12a_2010_p22.thy	11
isabelle/valid/amc12a_2011_p18.thy	12
isabelle/valid/amc12a_2013_p7.thy	19
isabelle/valid/amc12a_2013_p8.thy	29
isabelle/valid/amc12a_2015_p10.thy	14
isabelle/valid/amc12a_2016_p2.thy	12
isabelle/valid/amc12a_2016_p3.thy	12
isabelle/valid/amc12a_2017_p2.thy	14
isabelle/valid/amc12a_2017_p7.thy	14
isabelle/valid/amc12a_2019_p21.thy	12
isabelle/valid/amc12a_2019_p9.thy	15
isabelle/valid/amc12a_2020_p13.thy	15
isabelle/valid/amc12a_2020_p22.thy	12
isabelle/valid/amc12a_2021_p7.thy	12
isabelle/valid/amc12b_2002_p11.thy	14
isabelle/valid/amc12b_2002_p3.thy	31
isabelle/valid/amc12b_2002_p6.thy	16
isabelle/valid/amc12b_2003_p17.thy	22
isabelle/valid/amc12b_2003_p6.thy	14
isabelle/valid/amc12b_2003_p9.thy	13
isabelle/valid/amc12b_2004_p3.thy	12
isabelle/valid/amc12b_2020_p5.thy	13
isabelle/valid/amc12b_2021_p21.thy	13
isabelle/valid/imo_1961_p1.thy	18
isabelle/valid/imo_1962_p4.thy	14
isabelle/valid/imo_1964_p1_1.thy	12
isabelle/valid/imo_1964_p1_2.thy	11
isabelle/valid/imo_1965_p1.thy	17
isabelle/valid/imo_1966_p4.thy	14
isabelle/valid/imo_1966_p5.thy	21
isabelle/valid/imo_1967_p3.thy	16
isabelle/valid/imo_1973_p3.thy	12
isabelle/valid/imo_1974_p5.thy	12
isabelle/valid/imo_1977_p5.thy	14
isabelle/valid/imo_1978_p5.thy	16
isabelle/valid/imo_1979_p1.thy	14
isabelle/valid/imo_1984_p2.thy	16
isabelle/valid/imo_1987_p4.thy	11
isabelle/valid/imo_1987_p6.thy	15
isabelle/valid/imo_1988_p6.thy	13
isabelle/valid/imo_1990_p3.thy	13
isabelle/valid/imo_1993_p5.thy	12
isabelle/valid/imo_2006_p6.thy	12
isabelle/valid/induction_divisibility_3div2tooddnp1.thy	23
isabelle/valid/induction_divisibility_3divnto3m2n.thy	12
isabelle/valid/induction_divisibility_9div10tonm1.thy	12
isabelle/valid/induction_ineq_nsqlefactn.thy	44
isabelle/valid/induction_seq_mul2pnp1.thy	14
isabelle/valid/induction_sum2kp1npqsqm1.thy	12
isabelle/valid/induction_sum_1oktkp1.thy	11
isabelle/valid/induction_sum_odd.thy	12
isabelle/valid/mathd_algebra_10.thy	10
isabelle/valid/mathd_algebra_101.thy	25
isabelle/valid/mathd_algebra_104.thy	15
isabelle/valid/mathd_algebra_109.thy	13
isabelle/valid/mathd_algebra_11.thy	26
isabelle/valid/mathd_algebra_110.thy	13
isabelle/valid/mathd_algebra_116.thy	13
isabelle/valid/mathd_algebra_119.thy	13
isabelle/valid/mathd_algebra_123.thy	18
isabelle/valid/mathd_algebra_126.thy	17
isabelle/valid/mathd_algebra_13.thy	13
isabelle/valid/mathd_algebra_131.thy	16
isabelle/valid/mathd_algebra_132.thy	24
isabelle/valid/mathd_algebra_140.thy	13
isabelle/valid/mathd_algebra_144.thy	15
isabelle/valid/mathd_algebra_149.thy	14
isabelle/valid/mathd_algebra_15.thy	15
isabelle/valid/mathd_algebra_151.thy	11
isabelle/valid/mathd_algebra_159.thy	19
isabelle/valid/mathd_algebra_181.thy	20
isabelle/valid/mathd_algebra_182.thy	11
isabelle/valid/mathd_algebra_185.thy	12
isabelle/valid/mathd_algebra_190.thy	10
isabelle/valid/mathd_algebra_192.thy	15
isabelle/valid/mathd_algebra_206.thy	16
isabelle/valid/mathd_algebra_214.thy	18
isabelle/valid/mathd_algebra_22.thy	10
isabelle/valid/mathd_algebra_224.thy	11
isabelle/valid/mathd_algebra_234.thy	20
isabelle/valid/mathd_algebra_245.thy	36
isabelle/valid/mathd_algebra_247.thy	20
isabelle/valid/mathd_algebra_251.thy	13
isabelle/valid/mathd_algebra_267.thy	14
isabelle/valid/mathd_algebra_28.thy	14
isabelle/valid/mathd_algebra_282.thy	13
isabelle/valid/mathd_algebra_31.thy	14
isabelle/valid/mathd_algebra_323.thy	13
isabelle/valid/mathd_algebra_327.thy	12
isabelle/valid/mathd_algebra_35.thy	17
isabelle/valid/mathd_algebra_37.thy	17
isabelle/valid/mathd_algebra_393.thy	13
isabelle/valid/mathd_algebra_405.thy	27
isabelle/valid/mathd_algebra_410.thy	12
isabelle/valid/mathd_algebra_421.thy	16
isabelle/valid/mathd_algebra_422.thy	25
isabelle/valid/mathd_algebra_43.thy	22
isabelle/valid/mathd_algebra_433.thy	16
isabelle/valid/mathd_algebra_437.thy	16
isabelle/valid/mathd_algebra_451.thy	16
isabelle/valid/mathd_algebra_455.thy	17
isabelle/valid/mathd_algebra_462.thy	10
isabelle/valid/mathd_algebra_48.thy	14
isabelle/valid/mathd_algebra_480.thy	19
isabelle/valid/mathd_algebra_482.thy	19
isabelle/valid/mathd_algebra_493.thy	15
isabelle/valid/mathd_algebra_509.thy	10
isabelle/valid/mathd_algebra_51.thy	13
isabelle/valid/mathd_algebra_510.thy	13
isabelle/valid/mathd_algebra_536.thy	11
isabelle/valid/mathd_algebra_547.thy	15
isabelle/valid/mathd_algebra_55.thy	17
isabelle/valid/mathd_algebra_568.thy	11
isabelle/valid/mathd_algebra_59.thy	17
isabelle/valid/mathd_algebra_616.thy	16
isabelle/valid/mathd_algebra_67.thy	16
isabelle/valid/mathd_algebra_69.thy	13
isabelle/valid/mathd_algebra_73.thy	13
isabelle/valid/mathd_algebra_77.thy	16
isabelle/valid/mathd_algebra_89.thy	12
isabelle/valid/mathd_algebra_96.thy	15
isabelle/valid/mathd_numbertheory_101.thy	10
isabelle/valid/mathd_numbertheory_102.thy	10
isabelle/valid/mathd_numbertheory_109.thy	12
isabelle/valid/mathd_numbertheory_110.thy	14
isabelle/valid/mathd_numbertheory_126.thy	16
isabelle/valid/mathd_numbertheory_13.thy	18
isabelle/valid/mathd_numbertheory_132.thy	10
isabelle/valid/mathd_numbertheory_136.thy	11
isabelle/valid/mathd_numbertheory_149.thy	11
isabelle/valid/mathd_numbertheory_155.thy	10
isabelle/valid/mathd_numbertheory_156.thy	12
isabelle/valid/mathd_numbertheory_169.thy	10
isabelle/valid/mathd_numbertheory_188.thy	10
isabelle/valid/mathd_numbertheory_198.thy	10
isabelle/valid/mathd_numbertheory_200.thy	10
isabelle/valid/mathd_numbertheory_202.thy	10
isabelle/valid/mathd_numbertheory_211.thy	11
isabelle/valid/mathd_numbertheory_22.thy	13
isabelle/valid/mathd_numbertheory_221.thy	11
isabelle/valid/mathd_numbertheory_232.thy	16
isabelle/valid/mathd_numbertheory_236.thy	10
isabelle/valid/mathd_numbertheory_24.thy	10
isabelle/valid/mathd_numbertheory_252.thy	10
isabelle/valid/mathd_numbertheory_257.thy	13
isabelle/valid/mathd_numbertheory_269.thy	10
isabelle/valid/mathd_numbertheory_284.thy	20
isabelle/valid/mathd_numbertheory_30.thy	10
isabelle/valid/mathd_numbertheory_301.thy	13
isabelle/valid/mathd_numbertheory_303.thy	11
isabelle/valid/mathd_numbertheory_32.thy	11
isabelle/valid/mathd_numbertheory_326.thy	12
isabelle/valid/mathd_numbertheory_33.thy	13
isabelle/valid/mathd_numbertheory_335.thy	18
isabelle/valid/mathd_numbertheory_35.thy	11
isabelle/valid/mathd_numbertheory_37.thy	10
isabelle/valid/mathd_numbertheory_370.thy	12
isabelle/valid/mathd_numbertheory_403.thy	11
isabelle/valid/mathd_numbertheory_405.thy	18
isabelle/valid/mathd_numbertheory_412.thy	13
isabelle/valid/mathd_numbertheory_42.thy	16
isabelle/valid/mathd_numbertheory_43.thy	13
isabelle/valid/mathd_numbertheory_45.thy	8
isabelle/valid/mathd_numbertheory_458.thy	12
isabelle/valid/mathd_numbertheory_461.thy	13
isabelle/valid/mathd_numbertheory_466.thy	11
isabelle/valid/mathd_numbertheory_48.thy	13
isabelle/valid/mathd_numbertheory_530.thy	14
isabelle/valid/mathd_numbertheory_543.thy	10
isabelle/valid/mathd_numbertheory_629.thy	10
isabelle/valid/mathd_numbertheory_64.thy	11
isabelle/valid/mathd_numbertheory_640.thy	10
isabelle/valid/mathd_numbertheory_668.thy	15
isabelle/valid/mathd_numbertheory_690.thy	12
isabelle/valid/mathd_numbertheory_709.thy	15
isabelle/valid/mathd_numbertheory_739.thy	10
isabelle/valid/mathd_numbertheory_780.thy	15
isabelle/valid/mathd_numbertheory_81.thy	10
isabelle/valid/mathd_numbertheory_84.thy	10
isabelle/valid/mathd_numbertheory_92.thy	12
isabelle/valid/mathd_numbertheory_961.thy	10
isabelle/valid/numbertheory_2dvd4expn.thy	12
isabelle/valid/numbertheory_aneqprodakp4_anmsqrtanp1eq2.thy	13
isabelle/valid/numbertheory_nckeqnm1ckpnm1ckm1.thy	14
isabelle/valid/numbertheory_prmdvsneqnsqmodpeq0.thy	13
isabelle/valid/numbertheory_sqmod3in01d.thy	11
isabelle/valid/numbertheory_sqmod4in01d.thy	11
isabelle/valid/numbertheory_sumkmulnckeqnmul2pownm1.thy	14
isabelle/valid/numbertheory_xsqpysqintdenomeq.thy	13