src/HOL/ex/mesontest.ML
changeset 7183 9099542ee509
parent 6843 eeeddde75f3f
child 9092 a893887151c0
equal deleted inserted replaced
7182:090723b5024d 7183:9099542ee509
   589 by (safe_meson_tac 1);  
   589 by (safe_meson_tac 1);  
   590 result();
   590 result();
   591 
   591 
   592 writeln"Problem 66";  
   592 writeln"Problem 66";  
   593 Goal (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));
   593 Goal (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));
   594 (*TOO SLOW: more than 24 minutes!
   594 (*TOO SLOW, several minutes!  
       
   595      208346 inferences so far.  Searching to depth 23
   595 by (safe_meson_tac 1);
   596 by (safe_meson_tac 1);
   596 result();
   597 result();
   597 *)
   598 *)
   598 
   599 
   599 writeln"Problem 67";  
   600 writeln"Problem 67";