wneuper/isa: comparison src/Tools/isac/ProgLang/calculate.sml

equal deleted inserted replaced

-:dbc3a56ccd00
+:d9c3e373f8f5
 | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2)
 end
 | get_pair _ _ _ _ = NONE
 (*
->  val t = (term_of o the o (parse thy)) "#3 + #4";
+>  val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
 >  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  term2str t';
 >  atomty t';
 >
->  val t = (term_of o the o (parse thy)) "(a + #3) + #4";
+>  val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
+>  val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
+>  val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
 >  atomty t;
 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
 >  term2str t';
 >  val it = "#3 + (#4 + a) = #7 + a" : string
 >
 >
->  val t = (term_of o the o (parse thy)) "#-4//#-2";
+>  val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
 >  val eval_fn = the (assoc (!eval_list, "cancel"));
 >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "#2^^^#3";
+>  val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
 >  eval_binop "xxx" "pow" t thy;
 >  val eval_fn = (eval_binop "xxx")
 >		 : string -> term -> theory -> (string * term) option;
 >  val SOME (id,t') = get_pair thy "pow" eval_fn t;
 >  term2str t';
 >  val eval_fn = the (assoc (!eval_list, "pow"));
 >  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
+>  val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
 >  val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
 >  val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "#0 < #4";
+>  val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
 >  val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
 >  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
 >  term2str t';
->  val t = (term_of o the o (parse thy)) "#0 < #-4";
+>  val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
 >  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "#3 is_const";
+>  val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
 >  val eval_fn = the (assoc (!eval_list, "is'_const"));
 >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
 >  term2str t';
->  val t = (term_of o the o (parse thy)) "a is_const";
+>  val t = (Thm.term_of o the o (parse thy)) "a is_const";
 >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "#6//(#8::real)";
+>  val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
 >  val eval_fn = the (assoc (!eval_list, "cancel"));
 >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "sqrt #12";
+>  val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
 >  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
 >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
 >  term2str t';
 >  val it = "sqrt #12 = #2 * sqrt #3 " : string
 >
->  val t = (term_of o the o (parse thy)) "sqrt #9";
+>  val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
 >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
 >  term2str t';
 >
->  val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
+>  val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
 >  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
 >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
 >  term2str t';
 *)
 > get_calculation_ thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
 val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")
 -------------------------------------------------------------------6.8.02:
 val thy = SqRoot.thy;
-val t = (term_of o the o (parse thy)) "1+2";
+val t = (Thm.term_of o the o (parse thy)) "1+2";
 get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
 -------------------------------------------------------------------6.8.02:
-val t = (term_of o the o (parse thy)) "-1";
+val t = (Thm.term_of o the o (parse thy)) "-1";
 atomty t;
-val t = (term_of o the o (parse thy)) "0";
+val t = (Thm.term_of o the o (parse thy)) "0";
 atomty t;
-val t = (term_of o the o (parse thy)) "1";
+val t = (Thm.term_of o the o (parse thy)) "1";
 atomty t;
-val t = (term_of o the o (parse thy)) "2";
+val t = (Thm.term_of o the o (parse thy)) "2";
 atomty t;
-val t = (term_of o the o (parse thy)) "999999999";
+val t = (Thm.term_of o the o (parse thy)) "999999999";
 atomty t;
 -------------------------------------------------------------------6.8.02:
 > val ct = (the o (parse thy)) "a+#3+#4";
 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

changeset 59186	d9c3e373f8f5
parent 59185	dbc3a56ccd00
child 59255	383722bfcff5