Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/BridgeLibisabelle/use-cases.sml
changeset 60337 cbad4e18e91b
parent 60329 0c10aeff57d7
child 60389 81b98f7e9ea5
equal deleted inserted replaced
60336:dcb37736d573 60337:cbad4e18e91b 
   708  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   708  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   709  setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
 
   709  setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
 
   710  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   710  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   711  setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
 
   711  setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
 
   712  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   712  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   713  setNextTactic 1 (Rewrite ("all_left", ThmC.numerals_to_Free @{thm all_left}));
 
   713  setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
 
   714  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   714  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   715  setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
 
   715  setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
 
   716  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   716  autoCalculate 1 (Steps 1); fetchProposedTactic 1;
 
   717  (*               __________ for "16 + 12 * x = 0"*)
 
   717  (*               __________ for "16 + 12 * x = 0"*)
 
   718  setNextTactic 1 (Subproblem ("PolyEq",
 
   718  setNextTactic 1 (Subproblem ("PolyEq",
wneuper/isa