test/Tools/isac/BridgeLibisabelle/use-cases.sml
changeset 59902 e7910a62eaf2
parent 59898 68883c046963
child 59903 5037ca1b112b
equal deleted inserted replaced
59901:07a042166900 59902:e7910a62eaf2
   985 		  [Given ["fixedValues [r=Arbfix]"(*new input*)],
   985 		  [Given ["fixedValues [r=Arbfix]"(*new input*)],
   986 		   Find ["maximum b"(*new input*), "valuesFor"], 
   986 		   Find ["maximum b"(*new input*), "valuesFor"], 
   987 		   Relate ["relations"]],
   987 		   Relate ["relations"]],
   988 		  (*input (Arbfix will dissappear soon)*)
   988 		  (*input (Arbfix will dissappear soon)*)
   989 		  Pbl (*belongsto*),
   989 		  Pbl (*belongsto*),
   990 		  Spec.e_spec (*no input to the specification*));
   990 		  Spec.Spec.empty (*no input to the specification*));
   991 
   991 
   992  (*the user does not know, what 'superfluous' for 'maximum b' may mean
   992  (*the user does not know, what 'superfluous' for 'maximum b' may mean
   993   and asks what to do next*)
   993   and asks what to do next*)
   994  fetchProposedTactic 1;
   994  fetchProposedTactic 1;
   995  (*the student follows the advice*)
   995  (*the student follows the advice*)
   999  (*this input completes the model*)
   999  (*this input completes the model*)
  1000  modifyCalcHead 1 (([],Pbl), "not used here",
  1000  modifyCalcHead 1 (([],Pbl), "not used here",
  1001 		  [Given ["fixedValues [r=Arbfix]"],
  1001 		  [Given ["fixedValues [r=Arbfix]"],
  1002 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
  1002 		   Find ["maximum A", "valuesFor [a,b]"(*new input*)], 
  1003 		   Relate ["relations [A=a*b, \
  1003 		   Relate ["relations [A=a*b, \
  1004 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.e_spec);
  1004 			   \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.Spec.empty);
  1005 
  1005 
  1006  (*specification is not interesting and should be skipped by the dialogguide;
  1006  (*specification is not interesting and should be skipped by the dialogguide;
  1007    !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
  1007    !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
  1008  modifyCalcHead 1 (([],Pbl), "not used here",
  1008  modifyCalcHead 1 (([],Pbl), "not used here",
  1009 		  [Given ["fixedValues [r=Arbfix]"],
  1009 		  [Given ["fixedValues [r=Arbfix]"],