src/Tools/isac/Knowledge/PolyEq.thy
branchdecompose-isar
changeset 42133 f9a7294e6cd6
parent 41922 32d7766945fb
child 42197 7497ff20f1e8
equal deleted inserted replaced
42132:bf151bfd7e5b 42133:f9a7294e6cd6
  1101     "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^
  1101     "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^
  1102     "                  d1_polyeq_simplify   True))          @@  " ^
  1102     "                  d1_polyeq_simplify   True))          @@  " ^
  1103     "            (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^
  1103     "            (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^
  1104     "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
  1104     "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
  1105     " (L_L::bool list) = ((Or_to_List e_e)::bool list)            " ^
  1105     " (L_L::bool list) = ((Or_to_List e_e)::bool list)            " ^
  1106     " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
  1106     " in Check_elementwise L_L {(v_v::real). Assumptions} )"
  1107  ));
  1107  ));
  1108 *}
  1108 *}
  1109 ML{*
  1109 ML{*
  1110 store_met
  1110 store_met
  1111  (prep_met thy "met_polyeq_d22" [] e_metID
  1111  (prep_met thy "met_polyeq_d22" [] e_metID