1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Aug 27 10:28:44 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Aug 27 10:39:12 2010 +0200
1.3 @@ -2886,7 +2886,7 @@
1.4 val {rules, rew_ord=(_,ro),...} =
1.5 rep_rls (assoc_rls "rev_rew_p");
1.6
1.7 -val thy = Rational.thy;
1.8 +val thy = (theory "Rational");
1.9
1.10 (*.init_state = fn : term -> istate
1.11 initialzies the state of the script interpreter. The state is:
1.12 @@ -2904,7 +2904,7 @@
1.13 (#) could be extracted from here by (map #1)*).*)
1.14 (* val {rules, rew_ord=(_,ro),...} =
1.15 rep_rls (assoc_rls "rev_rew_p") (*USE ALWAYS, SEE val cancel_p*);
1.16 - val (thy, eval_rls, ro) =(Rational.thy, Atools_erls, ro) (*..val cancel_p*);
1.17 + val (thy, eval_rls, ro) =((theory "Rational"), Atools_erls, ro) (*..val cancel_p*);
1.18 val t = t;
1.19 *)
1.20 fun init_state thy eval_rls ro t =
1.21 @@ -2961,12 +2961,12 @@
1.22 value:
1.23 -> rule option: ... this rule is appropriate for cancellation;
1.24 there may be no such rule (if the term is canceled already.*)
1.25 -(* val thy = Rational.thy;
1.26 +(* val thy = (theory "Rational");
1.27 val Rrls {rew_ord=(_,ro),...} = cancel;
1.28 val ([rs],t) = (rss,f);
1.29 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
1.30
1.31 - val (thy, [rs]) = (Rational.thy, revsets);
1.32 + val (thy, [rs]) = ((theory "Rational"), revsets);
1.33 val Rrls {rew_ord=(_,ro),...} = cancel;
1.34 nex [rs] t;
1.35 *)
1.36 @@ -3003,7 +3003,7 @@
1.37 val cancel_p =
1.38 Rrls {id = "cancel_p", prepat=[],
1.39 rew_ord=("ord_make_polynomial",
1.40 - ord_make_polynomial false Rational.thy),
1.41 + ord_make_polynomial false (theory "Rational")),
1.42 erls = rational_erls,
1.43 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1.44 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.45 @@ -3036,7 +3036,7 @@
1.46 *)
1.47 val {rules=rules,rew_ord=(_,ro),...} =
1.48 rep_rls (assoc_rls "expand_binoms");
1.49 -val thy = Rational.thy;
1.50 +val thy = (theory "Rational");
1.51
1.52 fun init_state thy eval_rls ro t =
1.53 let val SOME (t',_) = factout_ thy t;
1.54 @@ -3086,7 +3086,7 @@
1.55 val cancel =
1.56 Rrls {id = "cancel", prepat=prepat,
1.57 rew_ord=("ord_make_polynomial",
1.58 - ord_make_polynomial false Rational.thy),
1.59 + ord_make_polynomial false (theory "Rational")),
1.60 erls = rational_erls,
1.61 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1.62 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.63 @@ -3112,7 +3112,7 @@
1.64 see rational.sml --- investigate rulesets for cancel_p ---*)
1.65 val {rules, rew_ord=(_,ro),...} =
1.66 rep_rls (assoc_rls "rev_rew_p");
1.67 -val thy = Rational.thy;
1.68 +val thy = (theory "Rational");
1.69
1.70
1.71 (*.common_nominator_p_ = fn : theory -> term -> (term * term list) option
1.72 @@ -3188,12 +3188,12 @@
1.73 value:
1.74 -> rule option: ... this rule is appropriate for cancellation;
1.75 there may be no such rule (if the term is canceled already.*)
1.76 -(* val thy = Rational.thy;
1.77 +(* val thy = (theory "Rational");
1.78 val Rrls {rew_ord=(_,ro),...} = cancel;
1.79 val ([rs],t) = (rss,f);
1.80 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
1.81
1.82 - val (thy, [rs]) = (Rational.thy, revsets);
1.83 + val (thy, [rs]) = ((theory "Rational"), revsets);
1.84 val Rrls {rew_ord=(_,ro),...} = cancel;
1.85 nex [rs] t;
1.86 *)
1.87 @@ -3240,7 +3240,7 @@
1.88 val common_nominator_p =
1.89 Rrls {id = "common_nominator_p", prepat=prepat,
1.90 rew_ord=("ord_make_polynomial",
1.91 - ord_make_polynomial false Rational.thy),
1.92 + ord_make_polynomial false (theory "Rational")),
1.93 erls = rational_erls,
1.94 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1.95 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.96 @@ -3261,7 +3261,7 @@
1.97
1.98 val {rules=rules,rew_ord=(_,ro),...} =
1.99 rep_rls (assoc_rls "make_polynomial");
1.100 -val thy = Rational.thy;
1.101 +val thy = (theory "Rational");
1.102
1.103
1.104 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
1.105 @@ -3337,12 +3337,12 @@
1.106 value:
1.107 -> rule option: ... this rule is appropriate for cancellation;
1.108 there may be no such rule (if the term is canceled already.*)
1.109 -(* val thy = Rational.thy;
1.110 +(* val thy = (theory "Rational");
1.111 val Rrls {rew_ord=(_,ro),...} = cancel;
1.112 val ([rs],t) = (rss,f);
1.113 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
1.114
1.115 - val (thy, [rs]) = (Rational.thy, revsets);
1.116 + val (thy, [rs]) = ((theory "Rational"), revsets);
1.117 val Rrls {rew_ord=(_,ro),...} = cancel_p;
1.118 nex [rs] t;
1.119 *)
1.120 @@ -3393,7 +3393,7 @@
1.121 val common_nominator =
1.122 Rrls {id = "common_nominator", prepat=prepat,
1.123 rew_ord=("ord_make_polynomial",
1.124 - ord_make_polynomial false Rational.thy),
1.125 + ord_make_polynomial false (theory "Rational")),
1.126 erls = rational_erls,
1.127 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1.128 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1.129 @@ -3611,10 +3611,6 @@
1.130 (*-------------------18.3.03 --> struct <-----------^^^--*)
1.131
1.132
1.133 -
1.134 -theory' := overwritel (!theory', [("Rational.thy",Rational.thy)]);
1.135 -
1.136 -
1.137 (*WN030318???SK: simplifies all but cancel and common_nominator*)
1.138 val simplify_rational =
1.139 merge_rls "simplify_rational" expand_binoms
1.140 @@ -3796,7 +3792,7 @@
1.141 (** problems **)
1.142
1.143 store_pbt
1.144 - (prep_pbt Rational.thy "pbl_simp_rat" [] e_pblID
1.145 + (prep_pbt (theory "Rational") "pbl_simp_rat" [] e_pblID
1.146 (["rational","simplification"],
1.147 [("#Given" ,["term t_"]),
1.148 ("#Where" ,["t_ is_ratpolyexp"]),
1.149 @@ -3811,7 +3807,7 @@
1.150 (*WN061025 this methods script is copied from (auto-generated) script
1.151 of norm_Rational in order to ease repair on inform*)
1.152 store_met
1.153 - (prep_met Rational.thy "met_simp_rat" [] e_metID
1.154 + (prep_met (theory "Rational") "met_simp_rat" [] e_metID
1.155 (["simplification","of_rationals"],
1.156 [("#Given" ,["term t_"]),
1.157 ("#Where" ,["t_ is_ratpolyexp"]),