test/Tools/isac/Knowledge/rateq.sml
branchdecompose-isar
changeset 41943 f33f6959948b
parent 41928 20138d6136cd
child 42394 977788dfed26
     1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Sat Mar 19 15:18:10 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Wed Mar 23 17:20:39 2011 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4  "---------(1/x=5) ---------------------";
     1.5  "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
     1.6  
     1.7 +(*=== inhibit exn ?=============================================================
     1.8 +
     1.9  val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in  x";
    1.10  val SOME(t_, _) = rewrite_set_ RatEq.thy  false RatEq_prls t;
    1.11  val result = term2str t_;
    1.12 @@ -143,3 +145,5 @@
    1.13  else  error "rateq.sml: new behaviour: [x = -2, x = 10]";
    1.14  
    1.15  "----------- rateq.sml end--------";
    1.16 +
    1.17 +===== inhibit exn ?===========================================================*)