1.1 --- a/test/Tools/isac/Test_Some.thy	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -1,45 +1,73 @@
     1.4 - 
     1.5  theory Test_Some imports Isac
     1.6 -begin ML_file "Knowledge/gcd_poly_ml.sml"
     1.7 -(*
     1.8 -declare [[show_types]] 
     1.9 -declare [[show_sorts]]
    1.10 -find_theorems "?a <= ?a"
    1.11 +begin 
    1.12 +ML_file "Knowledge/rational.sml"
    1.13  
    1.14 -print_facts
    1.15 -print_statement ""
    1.16 -print_theory
    1.17 -*)
    1.18 +section {* code for copy & paste ===============================================================*}
    1.19  ML {*
    1.20 -*}
    1.21 -ML {* (*==================*)
    1.22 -*}
    1.23 -ML {*
    1.24 -*}
    1.25 -ML {*
    1.26 -*}
    1.27 -ML {* (*==================*)
    1.28 -*}
    1.29 -ML {*
    1.30 -*}
    1.31 -ML {*
    1.32 -*}
    1.33 -ML {* (*==================*)
    1.34  "~~~~~ fun , args:"; val () = ();
    1.35 +"~~~~~ and , args:"; val () = ();
    1.36  
    1.37  "~~~~~ to  return val:"; val () = ();
    1.38  
    1.39  *}
    1.40 +text {*
    1.41 +  declare [[show_types]] 
    1.42 +  declare [[show_sorts]]
    1.43 +  find_theorems "?a <= ?a"
    1.44 +  
    1.45 +  print_facts
    1.46 +  print_statement ""
    1.47 +  print_theory
    1.48 +*}
    1.49 +ML {*
    1.50 +(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
    1.51 +============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
    1.52 +
    1.53 +(*========== inhibit exn WN130826 TODO =========================================================
    1.54 +============ inhibit exn WN130826 TODO ========================================================*)
    1.55 +
    1.56 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.57 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
    1.58 +
    1.59 +(*=========================^^^ correct until here ^^^==========================================*)
    1.60 +*}
    1.61 +
    1.62 +
    1.63 +section {* ====================================================================================*}
    1.64 +ML {*
    1.65 +*} ML {*
    1.66 +*} ML {*
    1.67 +*} ML {*
    1.68 +*} ML {*
    1.69 +*}
    1.70 +
    1.71 +section {* GREAT CONFUSION -> final hg ci =====================================================*}
    1.72 +ML {*
    1.73 +(*in isabisac12/test/../rational.sml*)
    1.74 +"-------- investigate rls common_nominator_p from OLD gcd --------------------";
    1.75 +(*ATTENTION:
    1.76 +val common_nominator_p =
    1.77 +  Rrls {id = "common_nominator_p", ...
    1.78 +	  scr = Rfuns {init_state  = init_state thy Atools_erls ro,
    1.79 +		  normal_form = add_fraction_p_ thy, <<<===================================
    1.80 +:
    1.81 +val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
    1.82 +(*but ^^^ not exported, just ^^^*)
    1.83 +
    1.84 +i.e. GREAT CONFUSION:
    1.85 +# normal_form of add_fractions_p is add_fraction_p_,
    1.86 +# and id of add_fractions_p is common_nominator_p
    1.87 +*)
    1.88 +
    1.89 +section {* ===================================================================================*}
    1.90 +ML {*
    1.91 +*} ML {*
    1.92 +*} ML {*
    1.93 +*}
    1.94 +
    1.95 +section {* ===================================================================================*}
    1.96 +ML {*
    1.97 +*} ML {*
    1.98 +*} ML {*
    1.99 +*}
   1.100  end
   1.101 -
   1.102 -(*========== inhibit exn WN1130701 broken already in 2009-2 =======================
   1.103 -============ inhibit exn WN1130701 broken already in 2009-2 =====================*)
   1.104 -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
   1.105 -============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
   1.106 -
   1.107 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   1.108 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
   1.109 -
   1.110 -(*=========================^^^ correct until here ^^^===========================*)
   1.111 -
   1.112 -