author | paulson |
Fri, 02 Jun 2000 18:30:38 +0200 | |
changeset 9025 | e50c0764e522 |
parent 9024 | b1f37f6819c4 |
child 9026 | 640c4fd8b5b3 |
--- a/src/HOL/UNITY/UNITY.ML Fri Jun 02 17:48:17 2000 +0200 +++ b/src/HOL/UNITY/UNITY.ML Fri Jun 02 18:30:38 2000 +0200 @@ -300,6 +300,11 @@ by (Blast_tac 1); qed "increasingD"; +Goalw [increasing_def, stable_def] "F : increasing (%s. c)"; +by Auto_tac; +qed "increasing_constant"; +AddIffs [increasing_constant]; + Goalw [increasing_def, stable_def, constrains_def] "mono g ==> increasing f <= increasing (g o f)"; by Auto_tac;