1.1 --- a/test/Tools/isac/Test_Some.thy	Sun Feb 19 10:04:04 2012 +0100
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Feb 20 18:18:03 2012 +0100
     1.3 @@ -1,116 +1,8 @@
     1.4   
     1.5  theory Test_Some imports Isac begin
     1.6  
     1.7 -use"../../../test/Tools/isac/Knowledge/isac.sml"
     1.8 +use"../../../test/Tools/isac/Knowledge/partial_fractions.sml"
     1.9  
    1.10 -ML {* (*================== redo thm.ML fun assbl_thm, 
    1.11 -  build Isac hangs: revert --all AFTER SAVING -- FOR DIFF !!!*)
    1.12 -*}
    1.13 -ML {*
    1.14 -*}
    1.15 -ML {*
    1.16 -*}
    1.17 -ML {* (*==================
    1.18 -  use"../../../test/Tools/isac/Knowledge/isac.sml"*) 
    1.19 -! ruleset';
    1.20 -*}
    1.21 -ML {*
    1.22 -isacrlsthms;
    1.23 -*}
    1.24 -ML {*
    1.25 -@{thm NTH_CONS}
    1.26 -(*"1 < ?n \<Longrightarrow> NTH ?n (?x # ?xs) = NTH (?n + - 1) ?xs"*)
    1.27 -*}
    1.28 -ML {*
    1.29 -Thm.derivation_name @{thm NTH_CONS}
    1.30 -*}
    1.31 -ML {*
    1.32 -val isacrlsthms = ! ruleset'
    1.33 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.34 -*}
    1.35 -ML {*
    1.36 -val isacrlsthms = ! ruleset'
    1.37 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.38 -  |> flat
    1.39 -*}
    1.40 -ML {*
    1.41 -val isacrlsthms = ! ruleset'
    1.42 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.43 -  |> flat
    1.44 -  |> map thm_of_thm
    1.45 -*}
    1.46 -ML {*
    1.47 -val isacrlsthms = ! ruleset'
    1.48 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
    1.49 -  |> flat
    1.50 -  |> map thm_of_thm
    1.51 -  |> gen_distinct Thm.eq_thm;
    1.52 -*}
    1.53 -ML {*
    1.54 -nth 3 isacrlsthms;
    1.55 -Thm.derivation_name (nth 3 isacrlsthms);
    1.56 -*}
    1.57 -ML {*
    1.58 -@{thm NTH_CONS};
    1.59 -Thm.derivation_name @{thm NTH_CONS};
    1.60 -*}
    1.61 -ML {*
    1.62 -Thm.derivation_name (num_str @{thm NTH_CONS})
    1.63 -*}
    1.64 -ML {*(*-------------------termC.sml, thm.ML-----vvvvv*)
    1.65 -*}
    1.66 -ML {* (*termC.sml*)
    1.67 -fun num_str thm =
    1.68 -  let val (deriv, 
    1.69 -	   {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, 
    1.70 -	    hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
    1.71 -    val prop' = numbers_to_string prop;
    1.72 -    val _ = writeln ("###in num_str: deriv= " ^ PolyML.makestring deriv);
    1.73 -    val thm = assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop'
    1.74 -    val _ = writeln ("###in num_str: derivation_name= " ^ Thm.derivation_name thm)
    1.75 -  in thm end;
    1.76 -*}
    1.77 -ML {*
    1.78 -val thm = @{thm NTH_CONS};
    1.79 -*}
    1.80 -ML {*
    1.81 -Thm.derivation_name (thm);
    1.82 -*}
    1.83 -ML {*
    1.84 -Thm.derivation_name (num_str thm);
    1.85 -*}
    1.86 -ML {*
    1.87 -Thm;       (*fn: string * thm -> rule            ... FROM ISAC !!!*)
    1.88 -rep_thm_G; (*fn: thm -> Basic_Thm.deriv * {hyps: ...*)
    1.89 -assbl_thm  (*fn: Basic_Thm.deriv -> theory_ref ->...*)
    1.90 -*}
    1.91 -ML {*
    1.92 -*}
    1.93 -ML {*
    1.94 -*}
    1.95 -ML {*
    1.96 -*}
    1.97 -ML {*(*-------------------termC.sml, thm.ML-----^^^^^*)
    1.98 -*}
    1.99 -ML {*
   1.100 -val isacrlsthms = ! ruleset'
   1.101 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   1.102 -  |> flat
   1.103 -  |> map thm_of_thm
   1.104 -  |> gen_distinct Thm.eq_thm
   1.105 -  |> map (` I)
   1.106 -*}
   1.107 -ML {*
   1.108 -val isacrlsthms = ! ruleset'
   1.109 -  |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*)
   1.110 -  |> flat
   1.111 -  |> map thm_of_thm
   1.112 -  |> gen_distinct Thm.eq_thm
   1.113 -  |> map (` I)
   1.114 -  |> map (apfst Thm.derivation_name)
   1.115 -*}
   1.116 -ML {*
   1.117 -*}
   1.118  ML {*
   1.119  *}
   1.120  ML {*