src/HOL/UNITY/UNITY.ML
changeset 9025 e50c0764e522
parent 9000 c20d58286a51
child 10064 1a77667b21ef
     1.1 --- a/src/HOL/UNITY/UNITY.ML	Fri Jun 02 17:48:17 2000 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY.ML	Fri Jun 02 18:30:38 2000 +0200
     1.3 @@ -300,6 +300,11 @@
     1.4  by (Blast_tac 1);
     1.5  qed "increasingD";
     1.6  
     1.7 +Goalw [increasing_def, stable_def] "F : increasing (%s. c)";
     1.8 +by Auto_tac; 
     1.9 +qed "increasing_constant";
    1.10 +AddIffs [increasing_constant];
    1.11 +
    1.12  Goalw [increasing_def, stable_def, constrains_def]
    1.13       "mono g ==> increasing f <= increasing (g o f)";
    1.14  by Auto_tac;