equal
deleted
inserted
replaced
937 theories |
937 theories |
938 NSPrimes |
938 NSPrimes |
939 |
939 |
940 session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + |
940 session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + |
941 description "Some arbitrary small test case for Mirabelle." |
941 description "Some arbitrary small test case for Mirabelle." |
942 options [timeout = 60, mirabelle_actions = "arith"] |
942 options [timeout = 60, |
|
943 mirabelle_theories = "HOL-Analysis.Inner_Product", mirabelle_actions = "arith"] |
943 sessions |
944 sessions |
944 "HOL-Analysis" |
945 "HOL-Analysis" |
945 theories |
946 theories |
946 "HOL-Analysis.Inner_Product" |
947 "HOL-Analysis.Inner_Product" |
947 |
948 |