Sets a lower value of Unify.search_bound
authorpaulson
Fri Mar 15 18:41:04 1996 +0100 (1996-03-15)
changeset 15843d59c407bd36
parent 1583 bc902840aab5
child 1585 c44a012cf950
Sets a lower value of Unify.search_bound
src/HOL/ex/MT.ML
     1.1 --- a/src/HOL/ex/MT.ML	Fri Mar 15 18:39:08 1996 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Fri Mar 15 18:41:04 1996 +0100
     1.3 @@ -17,6 +17,10 @@
     1.4  
     1.5  open MT;
     1.6  
     1.7 +(*Limit cyclic unifications during monotonicity proofs*)
     1.8 +val orig_search_bound = !Unify.search_bound;
     1.9 +Unify.search_bound := 8;
    1.10 +
    1.11  val prems = goal MT.thy "~a:{b} ==> ~a=b";
    1.12  by (cut_facts_tac prems 1);
    1.13  by (rtac notI 1);
    1.14 @@ -793,3 +797,8 @@
    1.15  by (dtac consistency 1);
    1.16  by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
    1.17  qed "basic_consistency";
    1.18 +
    1.19 +
    1.20 +Unify.search_bound := orig_search_bound;
    1.21 +
    1.22 +writeln"Reached end of file.";