equal
deleted
inserted
replaced
351 case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id) |
351 case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id) |
352 case _ => None |
352 case _ => None |
353 } |
353 } |
354 } |
354 } |
355 |
355 |
|
356 val SLEDGEHAMMER_PROVERS = "sledgehammer_provers" |
|
357 val Sledgehammer_Provers: Properties.T = List((FUNCTION, SLEDGEHAMMER_PROVERS)) |
|
358 |
356 object ML_Statistics |
359 object ML_Statistics |
357 { |
360 { |
358 def unapply(props: Properties.T): Option[Properties.T] = |
361 def unapply(props: Properties.T): Option[Properties.T] = |
359 props match { |
362 props match { |
360 case (FUNCTION, "ML_statistics") :: stats => Some(stats) |
363 case (FUNCTION, "ML_statistics") :: stats => Some(stats) |