Linting Isabelle/HOL

[TheMC47]

Description

This issue tracks the process of linting and fixing the warnings in Isabelle/HOL.

The lints used are:

• apply_isar_switch
• auto_structural_composition
• axiomatization_with_where
• bad_style_command
• complex_isar_initial_method
• counter_example_finder
• global_attribute_changes
• global_attribute_on_unnamed_lemma
• implicit_rule
• lemma_transforming_attribute
• low_level_apply_chain
• proof_finder
• tactic_proofs
• unrestricted_auto

Results

Below is a list of all the lints reported by the linter. Some of them might be false positives (e.g. using axiomatization with where is necessary in some places), but since lints cannot be disabled locally, these are also reported. A total of 431 lints were reported.

Theory: HOL.HOL

Lints:

• Lint name: axiomatization_with_where, location: 76:16, severity: error
• Lint name: axiomatization_with_where, location: 79:16, severity: error
• Lint name: axiomatization_with_where, location: 208:16, severity: error
• Lint name: axiomatization_with_where, location: 218:16, severity: error
• Lint name: axiomatization_with_where, location: 685:16, severity: error
• Lint name: implicit_rule, location: 748:6, severity: warn
• Lint name: implicit_rule, location: 751:6, severity: warn
• Lint name: implicit_rule, location: 754:6, severity: warn
• Lint name: implicit_rule, location: 1926:22, severity: warn

Theory: HOL.Orderings

Lints:

• Lint name: tactic_proofs, location: 1001:5, severity: error
• Lint name: tactic_proofs, location: 1005:5, severity: error
• Lint name: tactic_proofs, location: 1009:5, severity: error
• Lint name: tactic_proofs, location: 1013:5, severity: error
• Lint name: tactic_proofs, location: 1017:5, severity: error
• Lint name: tactic_proofs, location: 1021:5, severity: error
• Lint name: tactic_proofs, location: 1025:5, severity: error
• Lint name: tactic_proofs, location: 1029:5, severity: error

Theory: HOL.Set

Lints:

• Lint name: axiomatization_with_where, location: 19:3, severity: error

Theory: HOL.Fun

Lints:

• Lint name: complex_isar_initial_method, location: 382:7, severity: warn
• Lint name: complex_isar_initial_method, location: 386:9, severity: warn
• Lint name: complex_isar_initial_method, location: 428:9, severity: warn
• Lint name: complex_isar_initial_method, location: 637:9, severity: warn
• Lint name: tactic_proofs, location: 797:10, severity: error
• Lint name: tactic_proofs, location: 905:11, severity: error
• Lint name: tactic_proofs, location: 992:8, severity: error
• Lint name: tactic_proofs, location: 994:34, severity: error
• Lint name: tactic_proofs, location: 1002:18, severity: error

Theory: HOL.Complete_Lattices

Lints:

• Lint name: unrestricted_auto, location: 992:3, severity: error

Theory: HOL.Product_Type

Lints:

• Lint name: implicit_rule, location: 180:52, severity: warn
• Lint name: tactic_proofs, location: 697:16, severity: error
• Lint name: tactic_proofs, location: 705:16, severity: error
• Lint name: tactic_proofs, location: 713:16, severity: error
• Lint name: tactic_proofs, location: 721:16, severity: error
• Lint name: tactic_proofs, location: 729:16, severity: error
• Lint name: tactic_proofs, location: 856:9, severity: error

Theory: HOL.Rings

Lints:

• Lint name: implicit_rule, location: 194:17, severity: warn
• Lint name: tactic_proofs, location: 1178:31, severity: error
• Lint name: implicit_rule, location: 1545:7, severity: warn
• Lint name: tactic_proofs, location: 2042:31, severity: error
• Lint name: tactic_proofs, location: 2368:16, severity: error
• Lint name: complex_isar_initial_method, location: 2408:9, severity: warn

Theory: HOL.Nat

Lints:

• Lint name: axiomatization_with_where, location: 19:3, severity: error
• Lint name: tactic_proofs, location: 81:26, severity: error
• Lint name: tactic_proofs, location: 1088:18, severity: error
• Lint name: complex_isar_initial_method, location: 1127:9, severity: warn

Theory: HOL.Fields

Lints:

• Lint name: implicit_rule, location: 289:6, severity: warn
• Lint name: tactic_proofs, location: 522:7, severity: error
• Lint name: tactic_proofs, location: 650:7, severity: error

Theory: HOL.Finite_Set

Lints:

• Lint name: implicit_rule, location: 1229:15, severity: warn
• Lint name: implicit_rule, location: 1574:15, severity: warn
• Lint name: tactic_proofs, location: 1831:10, severity: error
• Lint name: lemma_transforming_attribute, location: 1952:23, severity: warn
• Lint name: tactic_proofs, location: 2361:14, severity: error

Theory: HOL.Relation

Lints:

• Lint name: unrestricted_auto, location: 1103:3, severity: error

Theory: HOL.Transitive_Closure

Lints:

• Lint name: tactic_proofs, location: 254:8, severity: error
• Lint name: complex_isar_initial_method, location: 1004:9, severity: warn
• Lint name: tactic_proofs, location: 1019:71, severity: error

Theory: HOL.Wellfounded

Lints:

• Lint name: tactic_proofs, location: 249:14, severity: error
• Lint name: tactic_proofs, location: 574:9, severity: error
• Lint name: tactic_proofs, location: 665:9, severity: error
• Lint name: complex_isar_initial_method, location: 741:7, severity: warn
• Lint name: tactic_proofs, location: 892:16, severity: error

Theory: HOL.Wfrec

Lints:

• Lint name: complex_isar_initial_method, location: 101:7, severity: warn

Theory: HOL.Order_Relation

Lints:

• Lint name: complex_isar_initial_method, location: 137:7, severity: warn
• Lint name: complex_isar_initial_method, location: 326:7, severity: warn
• Lint name: complex_isar_initial_method, location: 337:7, severity: warn
• Lint name: complex_isar_initial_method, location: 443:11, severity: warn
• Lint name: complex_isar_initial_method, location: 460:7, severity: warn
• Lint name: unrestricted_auto, location: 475:5, severity: error

Theory: HOL.BNF_Wellorder_Relation

Lints:

• Lint name: complex_isar_initial_method, location: 222:8, severity: warn
• Lint name: complex_isar_initial_method, location: 395:6, severity: warn
• Lint name: complex_isar_initial_method, location: 404:6, severity: warn
• Lint name: complex_isar_initial_method, location: 430:8, severity: warn
• Lint name: complex_isar_initial_method, location: 445:12, severity: warn
• Lint name: complex_isar_initial_method, location: 462:12, severity: warn

Theory: HOL.Hilbert_Choice

Lints:

• Lint name: axiomatization_with_where, location: 17:3, severity: error
• Lint name: complex_isar_initial_method, location: 429:7, severity: warn
• Lint name: complex_isar_initial_method, location: 523:7, severity: warn
• Lint name: complex_isar_initial_method, location: 984:9, severity: warn
• Lint name: complex_isar_initial_method, location: 1047:9, severity: warn
• Lint name: complex_isar_initial_method, location: 1057:9, severity: warn
• Lint name: complex_isar_initial_method, location: 1063:11, severity: warn
• Lint name: complex_isar_initial_method, location: 1175:16, severity: warn

Theory: HOL.BNF_Wellorder_Embedding

Lints:

• Lint name: complex_isar_initial_method, location: 144:6, severity: warn
• Lint name: complex_isar_initial_method, location: 181:8, severity: warn
• Lint name: complex_isar_initial_method, location: 271:6, severity: warn
• Lint name: complex_isar_initial_method, location: 302:8, severity: warn
• Lint name: complex_isar_initial_method, location: 353:8, severity: warn
• Lint name: complex_isar_initial_method, location: 448:9, severity: warn
• Lint name: complex_isar_initial_method, location: 555:8, severity: warn
• Lint name: complex_isar_initial_method, location: 727:10, severity: warn
• Lint name: complex_isar_initial_method, location: 814:6, severity: warn
• Lint name: complex_isar_initial_method, location: 863:8, severity: warn
• Lint name: tactic_proofs, location: 1044:11, severity: error
• Lint name: complex_isar_initial_method, location: 1062:8, severity: warn

Theory: HOL.BNF_Wellorder_Constructions

Lints:

• Lint name: complex_isar_initial_method, location: 110:6, severity: warn
• Lint name: complex_isar_initial_method, location: 123:8, severity: warn
• Lint name: complex_isar_initial_method, location: 163:8, severity: warn
• Lint name: complex_isar_initial_method, location: 289:8, severity: warn
• Lint name: complex_isar_initial_method, location: 713:6, severity: warn
• Lint name: complex_isar_initial_method, location: 778:6, severity: warn
• Lint name: complex_isar_initial_method, location: 931:6, severity: warn
• Lint name: complex_isar_initial_method, location: 952:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1095:8, severity: warn
• Lint name: complex_isar_initial_method, location: 1108:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1277:9, severity: warn
• Lint name: complex_isar_initial_method, location: 1283:11, severity: warn
• Lint name: complex_isar_initial_method, location: 1288:13, severity: warn
• Lint name: complex_isar_initial_method, location: 1294:15, severity: warn
• Lint name: complex_isar_initial_method, location: 1306:13, severity: warn
• Lint name: complex_isar_initial_method, location: 1312:15, severity: warn
• Lint name: complex_isar_initial_method, location: 1318:17, severity: warn
• Lint name: complex_isar_initial_method, location: 1332:11, severity: warn
• Lint name: complex_isar_initial_method, location: 1336:13, severity: warn
• Lint name: complex_isar_initial_method, location: 1342:15, severity: warn
• Lint name: complex_isar_initial_method, location: 1348:17, severity: warn
• Lint name: complex_isar_initial_method, location: 1361:13, severity: warn
• Lint name: complex_isar_initial_method, location: 1367:15, severity: warn
• Lint name: complex_isar_initial_method, location: 1391:6, severity: warn
• Lint name: unrestricted_auto, location: 1575:1, severity: error

Theory: HOL.Zorn

Lints:

• Lint name: complex_isar_initial_method, location: 518:11, severity: warn
• Lint name: complex_isar_initial_method, location: 529:11, severity: warn
• Lint name: complex_isar_initial_method, location: 691:7, severity: warn
• Lint name: complex_isar_initial_method, location: 718:7, severity: warn

Theory: HOL.BNF_Cardinal_Order_Relation

Lints:

• Lint name: complex_isar_initial_method, location: 89:6, severity: warn
• Lint name: complex_isar_initial_method, location: 151:6, severity: warn
• Lint name: complex_isar_initial_method, location: 176:6, severity: warn
• Lint name: complex_isar_initial_method, location: 389:6, severity: warn
• Lint name: complex_isar_initial_method, location: 606:6, severity: warn
• Lint name: complex_isar_initial_method, location: 846:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1020:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1060:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1087:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1236:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1351:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1533:32, severity: warn
• Lint name: complex_isar_initial_method, location: 1564:35, severity: warn
• Lint name: apply_isar_switch, location: 1657:30, severity: warn

Theory: HOL.BNF_Cardinal_Arithmetic

Lints:

• Lint name: unrestricted_auto, location: 75:1, severity: error
• Lint name: low_level_apply_chain, location: 76:1, severity: info
• Lint name: low_level_apply_chain, location: 531:5, severity: info
• Lint name: low_level_apply_chain, location: 554:5, severity: info

Theory: HOL.BNF_Composition

Lints:

• Lint name: low_level_apply_chain, location: 32:3, severity: info
• Lint name: unrestricted_auto, location: 170:3, severity: error

Theory: HOL.BNF_Fixpoint_Base

Lints:

• Lint name: implicit_rule, location: 142:24, severity: warn

Theory: HOL.Transfer

Lints:

• Lint name: global_attribute_on_unnamed_lemma, location: 206:8, severity: error
• Lint name: global_attribute_on_unnamed_lemma, location: 211:8, severity: error
• Lint name: tactic_proofs, location: 535:53, severity: error
• Lint name: complex_isar_initial_method, location: 623:6, severity: warn

Theory: HOL.Num

Lints:

• Lint name: tactic_proofs, location: 397:12, severity: error
• Lint name: tactic_proofs, location: 398:12, severity: error
• Lint name: tactic_proofs, location: 402:10, severity: error
• Lint name: tactic_proofs, location: 403:10, severity: error
• Lint name: low_level_apply_chain, location: 396:7, severity: info
• Lint name: low_level_apply_chain, location: 1519:5, severity: info

Theory: HOL.Power

Lints:

• Lint name: tactic_proofs, location: 371:51, severity: error
• Lint name: lemma_transforming_attribute, location: 494:26, severity: warn
• Lint name: lemma_transforming_attribute, location: 505:32, severity: warn
• Lint name: unrestricted_auto, location: 512:5, severity: error
• Lint name: tactic_proofs, location: 513:11, severity: error
• Lint name: unrestricted_auto, location: 528:5, severity: error
• Lint name: tactic_proofs, location: 529:11, severity: error
• Lint name: unrestricted_auto, location: 555:5, severity: error
• Lint name: tactic_proofs, location: 556:11, severity: error
• Lint name: unrestricted_auto, location: 574:5, severity: error
• Lint name: tactic_proofs, location: 575:11, severity: error

Theory: HOL.Groups_Big

Lints:

• Lint name: unrestricted_auto, location: 1017:5, severity: error
• Lint name: implicit_rule, location: 1450:37, severity: warn

Theory: HOL.Equiv_Relations

Lints:

• Lint name: complex_isar_initial_method, location: 268:9, severity: warn
• Lint name: complex_isar_initial_method, location: 425:9, severity: warn

Theory: HOL.Lifting_Set

Lints:

• Lint name: complex_isar_initial_method, location: 315:7, severity: warn
• Lint name: unrestricted_auto, location: 354:7, severity: error

Theory: HOL.Lattices_Big

Lints:

• Lint name: tactic_proofs, location: 1052:9, severity: error

Theory: HOL.Partial_Function

Lints:

• Lint name: tactic_proofs, location: 223:8, severity: error
• Lint name: tactic_proofs, location: 224:7, severity: error

Theory: HOL.Fun_Def

Lints:

• Lint name: unrestricted_auto, location: 53:3, severity: error
• Lint name: unrestricted_auto, location: 247:3, severity: error
• Lint name: implicit_rule, location: 249:9, severity: warn
• Lint name: unrestricted_auto, location: 270:3, severity: error

Theory: HOL.Quotient

Lints:

• Lint name: tactic_proofs, location: 151:8, severity: error
• Lint name: complex_isar_initial_method, location: 327:7, severity: warn
• Lint name: unrestricted_auto, location: 425:3, severity: error
• Lint name: implicit_rule, location: 545:12, severity: warn

Theory: HOL.Int

Lints:

• Lint name: complex_isar_initial_method, location: 56:7, severity: warn
• Lint name: tactic_proofs, location: 143:8, severity: error
• Lint name: tactic_proofs, location: 152:8, severity: error
• Lint name: tactic_proofs, location: 192:8, severity: error
• Lint name: tactic_proofs, location: 478:8, severity: error
• Lint name: tactic_proofs, location: 484:8, severity: error
• Lint name: tactic_proofs, location: 741:8, severity: error
• Lint name: unrestricted_auto, location: 1153:5, severity: error
• Lint name: tactic_proofs, location: 1428:8, severity: error

Theory: HOL.Euclidean_Division

Lints:

• Lint name: tactic_proofs, location: 102:56, severity: error
• Lint name: implicit_rule, location: 142:7, severity: warn

Theory: HOL.Divides

Lints:

• Lint name: tactic_proofs, location: 43:6, severity: error
• Lint name: tactic_proofs, location: 54:7, severity: error
• Lint name: tactic_proofs, location: 448:14, severity: error
• Lint name: unrestricted_auto, location: 486:54, severity: error
• Lint name: unrestricted_auto, location: 585:4, severity: error
• Lint name: implicit_rule, location: 675:38, severity: warn
• Lint name: tactic_proofs, location: 684:28, severity: error
• Lint name: tactic_proofs, location: 688:28, severity: error
• Lint name: tactic_proofs, location: 688:56, severity: error
• Lint name: tactic_proofs, location: 743:32, severity: error

Theory: HOL.Set_Interval

Lints:

• Lint name: unrestricted_auto, location: 462:3, severity: error
• Lint name: tactic_proofs, location: 939:23, severity: error
• Lint name: unrestricted_auto, location: 989:3, severity: error
• Lint name: tactic_proofs, location: 990:10, severity: error
• Lint name: unrestricted_auto, location: 1142:3, severity: error
• Lint name: tactic_proofs, location: 1143:9, severity: error
• Lint name: tactic_proofs, location: 1217:5, severity: error
• Lint name: implicit_rule, location: 1313:31, severity: warn
• Lint name: unrestricted_auto, location: 1325:4, severity: error
• Lint name: unrestricted_auto, location: 1341:5, severity: error
• Lint name: tactic_proofs, location: 1342:11, severity: error
• Lint name: complex_isar_initial_method, location: 1428:9, severity: warn
• Lint name: unrestricted_auto, location: 1476:3, severity: error
• Lint name: tactic_proofs, location: 1477:9, severity: error
• Lint name: unrestricted_auto, location: 1693:3, severity: error
• Lint name: implicit_rule, location: 1722:6, severity: warn
• Lint name: unrestricted_auto, location: 2314:36, severity: error

Theory: HOL.Conditionally_Complete_Lattices

Lints:

• Lint name: complex_isar_initial_method, location: 504:7, severity: warn
• Lint name: unrestricted_auto, location: 511:5, severity: error
• Lint name: tactic_proofs, location: 527:11, severity: error
• Lint name: unrestricted_auto, location: 768:1, severity: error
• Lint name: unrestricted_auto, location: 815:3, severity: error

Theory: HOL.Filter

Lints:

• Lint name: complex_isar_initial_method, location: 442:9, severity: warn
• Lint name: unrestricted_auto, location: 1294:3, severity: error
• Lint name: complex_isar_initial_method, location: 1448:7, severity: warn
• Lint name: tactic_proofs, location: 1498:27, severity: error
• Lint name: tactic_proofs, location: 1509:25, severity: error
• Lint name: tactic_proofs, location: 1519:25, severity: error
• Lint name: complex_isar_initial_method, location: 1564:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1808:6, severity: warn
• Lint name: complex_isar_initial_method, location: 1885:6, severity: warn

Theory: HOL.Presburger

Lints:

• Lint name: unrestricted_auto, location: 57:1, severity: error
• Lint name: tactic_proofs, location: 170:38, severity: error
• Lint name: tactic_proofs, location: 353:9, severity: error
• Lint name: tactic_proofs, location: 355:10, severity: error
• Lint name: tactic_proofs, location: 360:9, severity: error
• Lint name: low_level_apply_chain, location: 356:3, severity: info

Theory: HOL.List

Lints:

• Lint name: tactic_proofs, location: 894:31, severity: error
• Lint name: tactic_proofs, location: 934:32, severity: error
• Lint name: tactic_proofs, location: 1062:15, severity: error
• Lint name: tactic_proofs, location: 1220:9, severity: error
• Lint name: implicit_rule, location: 1369:5, severity: warn
• Lint name: implicit_rule, location: 1396:6, severity: warn
• Lint name: tactic_proofs, location: 1905:44, severity: error
• Lint name: tactic_proofs, location: 2104:38, severity: error
• Lint name: tactic_proofs, location: 2107:38, severity: error
• Lint name: tactic_proofs, location: 2110:38, severity: error
• Lint name: tactic_proofs, location: 2113:38, severity: error
• Lint name: tactic_proofs, location: 2135:38, severity: error
• Lint name: tactic_proofs, location: 2139:38, severity: error
• Lint name: tactic_proofs, location: 2679:33, severity: error
• Lint name: tactic_proofs, location: 2883:11, severity: error
• Lint name: tactic_proofs, location: 2884:11, severity: error
• Lint name: tactic_proofs, location: 2900:11, severity: error
• Lint name: tactic_proofs, location: 2901:11, severity: error
• Lint name: unrestricted_auto, location: 3685:5, severity: error
• Lint name: unrestricted_auto, location: 3748:5, severity: error
• Lint name: unrestricted_auto, location: 4246:5, severity: error
• Lint name: tactic_proofs, location: 4348:3, severity: error
• Lint name: unrestricted_auto, location: 4800:14, severity: error
• Lint name: tactic_proofs, location: 5073:57, severity: error
• Lint name: tactic_proofs, location: 5080:56, severity: error
• Lint name: tactic_proofs, location: 5081:57, severity: error
• Lint name: unrestricted_auto, location: 5226:7, severity: error
• Lint name: tactic_proofs, location: 5847:8, severity: error
• Lint name: tactic_proofs, location: 6526:13, severity: error
• Lint name: tactic_proofs, location: 6527:12, severity: error
• Lint name: tactic_proofs, location: 6721:24, severity: error
• Lint name: tactic_proofs, location: 6724:24, severity: error
• Lint name: complex_isar_initial_method, location: 6868:7, severity: warn
• Lint name: tactic_proofs, location: 7081:30, severity: error
• Lint name: tactic_proofs, location: 7087:30, severity: error
• Lint name: tactic_proofs, location: 7090:31, severity: error
• Lint name: tactic_proofs, location: 7108:33, severity: error

Theory: HOL.Groups_List

Lints:

• Lint name: unrestricted_auto, location: 197:2, severity: error

Theory: HOL.Factorial

Lints:

• Lint name: unrestricted_auto, location: 68:3, severity: error

Theory: HOL.Binomial

Lints:

• Lint name: implicit_rule, location: 69:8, severity: warn
• Lint name: auto_structural_composition, location: 69:13, severity: info
• Lint name: unrestricted_auto, location: 1049:7, severity: error
• Lint name: unrestricted_auto, location: 1056:5, severity: error
• Lint name: tactic_proofs, location: 1269:33, severity: error

Theory: HOL.Map

Lints:

• Lint name: unrestricted_auto, location: 472:7, severity: error

Theory: HOL.Enum

Lints:

• Lint name: unrestricted_auto, location: 361:7, severity: error
• Lint name: tactic_proofs, location: 362:13, severity: error
• Lint name: unrestricted_auto, location: 536:1, severity: error
• Lint name: unrestricted_auto, location: 641:1, severity: error

Theory: HOL.Bit_Operations

Lints:

• Lint name: unrestricted_auto, location: 449:5, severity: error
• Lint name: unrestricted_auto, location: 462:5, severity: error
• Lint name: unrestricted_auto, location: 624:5, severity: error
• Lint name: unrestricted_auto, location: 625:6, severity: error
• Lint name: unrestricted_auto, location: 639:5, severity: error
• Lint name: implicit_rule, location: 665:10, severity: warn
• Lint name: unrestricted_auto, location: 934:5, severity: error
• Lint name: unrestricted_auto, location: 1426:3, severity: error
• Lint name: unrestricted_auto, location: 2244:7, severity: error

Theory: HOL.Code_Numeral

Lints:

• Lint name: implicit_rule, location: 20:15, severity: warn
• Lint name: implicit_rule, location: 28:15, severity: warn
• Lint name: implicit_rule, location: 32:15, severity: warn
• Lint name: implicit_rule, location: 121:15, severity: warn
• Lint name: implicit_rule, location: 129:15, severity: warn
• Lint name: implicit_rule, location: 133:15, severity: warn
• Lint name: implicit_rule, location: 157:15, severity: warn
• Lint name: implicit_rule, location: 161:15, severity: warn
• Lint name: implicit_rule, location: 165:15, severity: warn
• Lint name: implicit_rule, location: 237:15, severity: warn
• Lint name: implicit_rule, location: 241:15, severity: warn
• Lint name: implicit_rule, location: 877:15, severity: warn
• Lint name: implicit_rule, location: 885:15, severity: warn
• Lint name: implicit_rule, location: 889:15, severity: warn
• Lint name: implicit_rule, location: 967:15, severity: warn
• Lint name: implicit_rule, location: 971:15, severity: warn
• Lint name: implicit_rule, location: 975:15, severity: warn
• Lint name: implicit_rule, location: 979:15, severity: warn
• Lint name: implicit_rule, location: 1021:15, severity: warn
• Lint name: implicit_rule, location: 1025:15, severity: warn
• Lint name: implicit_rule, location: 1176:15, severity: warn
• Lint name: implicit_rule, location: 1180:15, severity: warn

Theory: HOL.GCD

Lints:

• Lint name: implicit_rule, location: 284:6, severity: warn
• Lint name: implicit_rule, location: 572:6, severity: warn
• Lint name: implicit_rule, location: 1231:6, severity: warn
• Lint name: implicit_rule, location: 1591:7, severity: warn
• Lint name: tactic_proofs, location: 2192:11, severity: error
• Lint name: tactic_proofs, location: 2193:11, severity: error
• Lint name: unrestricted_auto, location: 2272:3, severity: error
• Lint name: tactic_proofs, location: 2274:9, severity: error

Theory: HOL.String

Lints:

• Lint name: implicit_rule, location: 142:8, severity: warn
• Lint name: implicit_rule, location: 393:15, severity: warn

Theory: HOL.BNF_Greatest_Fixpoint

Lints:

• Lint name: complex_isar_initial_method, location: 253:7, severity: warn

Theory: HOL.Predicate

Lints:

• Lint name: complex_isar_initial_method, location: 107:9, severity: warn
• Lint name: low_level_apply_chain, location: 360:5, severity: info

Theory: HOL.Code_Evaluation

Lints:

• Lint name: lemma_transforming_attribute, location: 123:24, severity: warn

Theory: HOL.Record

Lints:

• Lint name: tactic_proofs, location: 140:9, severity: error
• Lint name: implicit_rule, location: 155:6, severity: warn

Theory: HOL.Nitpick

Lints:

• Lint name: tactic_proofs, location: 43:10, severity: error
• Lint name: low_level_apply_chain, location: 38:3, severity: info
• Lint name: unrestricted_auto, location: 93:4, severity: error
• Lint name: tactic_proofs, location: 99:9, severity: error

Theory: HOL.Archimedean_Field

Lints:

• Lint name: unrestricted_auto, location: 712:5, severity: error
• Lint name: unrestricted_auto, location: 727:3, severity: error
• Lint name: unrestricted_auto, location: 736:3, severity: error

Theory: HOL.Modules

Lints:

• Lint name: tactic_proofs, location: 312:11, severity: error
• Lint name: tactic_proofs, location: 313:11, severity: error
• Lint name: unrestricted_auto, location: 327:5, severity: error
• Lint name: tactic_proofs, location: 439:11, severity: error
• Lint name: unrestricted_auto, location: 921:3, severity: error

Theory: HOL.Rat

Lints:

• Lint name: complex_isar_initial_method, location: 447:7, severity: warn

Theory: HOL.Real

Lints:

• Lint name: complex_isar_initial_method, location: 99:9, severity: warn
• Lint name: complex_isar_initial_method, location: 166:9, severity: warn
• Lint name: complex_isar_initial_method, location: 243:9, severity: warn
• Lint name: complex_isar_initial_method, location: 310:9, severity: warn
• Lint name: complex_isar_initial_method, location: 344:9, severity: warn
• Lint name: complex_isar_initial_method, location: 536:11, severity: warn
• Lint name: tactic_proofs, location: 656:13, severity: error
• Lint name: complex_isar_initial_method, location: 724:11, severity: warn
• Lint name: complex_isar_initial_method, location: 1118:9, severity: warn
• Lint name: complex_isar_initial_method, location: 1129:7, severity: warn
• Lint name: unrestricted_auto, location: 1383:3, severity: error

Theory: HOL.Vector_Spaces

Lints:

• Lint name: tactic_proofs, location: 329:15, severity: error
• Lint name: complex_isar_initial_method, location: 748:7, severity: warn
• Lint name: tactic_proofs, location: 1070:15, severity: error
• Lint name: complex_isar_initial_method, location: 1241:9, severity: warn

Theory: HOL.Topological_Spaces

Lints:

• Lint name: tactic_proofs, location: 557:25, severity: error
• Lint name: tactic_proofs, location: 967:25, severity: error
• Lint name: tactic_proofs, location: 1003:25, severity: error
• Lint name: complex_isar_initial_method, location: 2546:7, severity: warn
• Lint name: tactic_proofs, location: 2819:11, severity: error
• Lint name: tactic_proofs, location: 2820:11, severity: error
• Lint name: tactic_proofs, location: 3306:27, severity: error
• Lint name: tactic_proofs, location: 3400:10, severity: error
• Lint name: complex_isar_initial_method, location: 3586:7, severity: warn

Theory: HOL.Real_Vector_Spaces

Lints:

• Lint name: unrestricted_auto, location: 555:3, severity: error
• Lint name: tactic_proofs, location: 707:6, severity: error
• Lint name: tactic_proofs, location: 1580:8, severity: error
• Lint name: tactic_proofs, location: 1588:8, severity: error
• Lint name: tactic_proofs, location: 1703:8, severity: error
• Lint name: tactic_proofs, location: 1765:8, severity: error
• Lint name: tactic_proofs, location: 1848:10, severity: error
• Lint name: complex_isar_initial_method, location: 1872:7, severity: warn
• Lint name: unrestricted_auto, location: 2096:3, severity: error
• Lint name: complex_isar_initial_method, location: 2227:7, severity: warn
• Lint name: unrestricted_auto, location: 2230:5, severity: error
• Lint name: unrestricted_auto, location: 2261:45, severity: error

Theory: HOL.Limits

Lints:

• Lint name: tactic_proofs, location: 47:8, severity: error
• Lint name: tactic_proofs, location: 364:11, severity: error
• Lint name: complex_isar_initial_method, location: 372:9, severity: warn
• Lint name: complex_isar_initial_method, location: 415:11, severity: warn
• Lint name: unrestricted_auto, location: 432:9, severity: error

Theory: HOL.Deriv

Lints:

• Lint name: complex_isar_initial_method, location: 1355:11, severity: warn
• Lint name: complex_isar_initial_method, location: 1392:11, severity: warn
• Lint name: tactic_proofs, location: 1489:8, severity: error
• Lint name: tactic_proofs, location: 1493:8, severity: error
• Lint name: tactic_proofs, location: 1918:8, severity: error
• Lint name: complex_isar_initial_method, location: 2070:9, severity: warn
• Lint name: tactic_proofs, location: 2153:8, severity: error
• Lint name: tactic_proofs, location: 2159:8, severity: error
• Lint name: tactic_proofs, location: 2392:9, severity: error
• Lint name: tactic_proofs, location: 2406:7, severity: error
• Lint name: tactic_proofs, location: 2419:7, severity: error

Theory: HOL.NthRoot

Lints:

• Lint name: complex_isar_initial_method, location: 129:7, severity: warn
• Lint name: unrestricted_auto, location: 551:3, severity: error
• Lint name: unrestricted_auto, location: 628:3, severity: error
• Lint name: low_level_apply_chain, location: 701:3, severity: info
• Lint name: unrestricted_auto, location: 717:4, severity: error

Theory: HOL.Series

Lints:

• Lint name: complex_isar_initial_method, location: 276:7, severity: warn
• Lint name: complex_isar_initial_method, location: 790:9, severity: warn
• Lint name: complex_isar_initial_method, location: 937:9, severity: warn

Theory: HOL.Transcendental

Lints:

• Lint name: tactic_proofs, location: 947:25, severity: error
• Lint name: tactic_proofs, location: 991:11, severity: error
• Lint name: complex_isar_initial_method, location: 2270:7, severity: warn
• Lint name: complex_isar_initial_method, location: 2587:7, severity: warn
• Lint name: tactic_proofs, location: 4095:8, severity: error
• Lint name: tactic_proofs, location: 4174:10, severity: error
• Lint name: complex_isar_initial_method, location: 4363:9, severity: warn
• Lint name: tactic_proofs, location: 4673:8, severity: error
• Lint name: tactic_proofs, location: 5376:8, severity: error
• Lint name: tactic_proofs, location: 6161:11, severity: error
• Lint name: tactic_proofs, location: 6773:42, severity: error

Theory: HOL.Complex

Lints:

• Lint name: unrestricted_auto, location: 423:10, severity: error
• Lint name: unrestricted_auto, location: 780:6, severity: error
• Lint name: tactic_proofs, location: 781:12, severity: error
• Lint name: unrestricted_auto, location: 782:6, severity: error
• Lint name: tactic_proofs, location: 936:9, severity: error
• Lint name: unrestricted_auto, location: 937:3, severity: error
• Lint name: tactic_proofs, location: 938:9, severity: error
• Lint name: complex_isar_initial_method, location: 998:7, severity: warn

Theory: HOL.MacLaurin

Lints:

• Lint name: complex_isar_initial_method, location: 39:7, severity: warn
• Lint name: complex_isar_initial_method, location: 581:9, severity: warn