val {ppc,...} = get_pbt pI

 	val {ppc,...} = get_pbt pI

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its = add_id its_

 	val its = add_id its_

 	val pits = map flattup2 its

 	val pits = map flattup2 its

 	val (pI, mI) = if mI <> ["no_met"] then (pI, mI)

 	val (pI, mI) = if mI <> ["no_met"] then (pI, mI)

 			in (pI, (hd o #met o get_pbt) pI) end

 			in (pI, (hd o #met o get_pbt) pI) end

 	val {ppc,pre,prls,...} = get_met mI

 	val {ppc,pre,prls,...} = get_met mI

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its = add_id its_

 	val its = add_id its_

 	val mits = map flattup2 its

 	val mits = map flattup2 its

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its = add_id its_

 	val its = add_id its_

 	val pits = map flattup2 its

 	val pits = map flattup2 its

 	val (pI, mI) = if mI <> ["no_met"] then (pI, mI)

 	val (pI, mI) = if mI <> ["no_met"] then (pI, mI)

 		   else case refine_pbl thy pI pits of

 		   else case refine_pbl thy pI pits of

 	val {ppc,pre,prls,...} = get_met mI

 	val {ppc,pre,prls,...} = get_met mI

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)

 	val its = add_id its_

 	val its = add_id its_

 	val mits = map flattup2 its

 	val mits = map flattup2 its

 	val pre = check_preconds thy prls pre mits

 	val pre = check_preconds thy prls pre mits

 (* val hdt = ifo;

 (* val hdt = ifo;

    *)

    *)

 fun cas_input hdt =

 fun cas_input hdt =

     let val (h,argl) = strip_comb hdt

     let val (h,argl) = strip_comb hdt

     in case assoc (!castab, h) of

     in case assoc (!castab, h) of

 	 (*let val (pt,_) = 

 	 (*let val (pt,_) = 

 		   cappend_problem e_ptree [] e_istate 

 		   cappend_problem e_ptree [] e_istate 

 				   ([], e_spec) ([], e_spec, e_term)

 				   ([], e_spec) ([], e_spec, e_term)

 	   in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),

 	   in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),

 		    [], [], e_spec)) end*)

 		    [], [], e_spec)) end*)

 	    *)

 	    *)

 	   let val dtss = argl2dtss argl

 	   let val dtss = argl2dtss argl

 	       val (pI, pits, mI, mits, pre) = cas_input_ spec dtss

 	       val (pI, pits, mI, mits, pre) = cas_input_ spec dtss

 	       val spec = (dI, pI, mI)

 	       val spec = (dI, pI, mI)

 	       val (pt,_) = 

 	       val (pt,_) = 

 		   cappend_problem e_ptree [] e_istate ([], e_spec) 

 		   cappend_problem e_ptree [] e_istate ([], e_spec) 

 				   ([], e_spec, hdt)

 				   ([], e_spec, hdt)

 	       val pt = update_spec pt [] spec

 	       val pt = update_spec pt [] spec

 	       val pt = update_pbl pt [] pits

 	       val pt = update_pbl pt [] pits

 	       val pt = update_met pt [] mits

 	       val pt = update_met pt [] mits

     end;

     end;

 (*lazy evaluation for Isac.thy*)

 (*lazy evaluation for Isac.thy*)

 fun Isac _  = assoc_thy "Isac.thy";

 fun Isac _  = assoc_thy "Isac.thy";

    *)

    *)

 fun appl_add' dI oris ppc pbt (sel, ct) = 

 fun appl_add' dI oris ppc pbt (sel, ct) = 

     let 

     let 

 	val thy = assoc_thy dI;

 	val thy = assoc_thy dI;

     in case parse thy ct of

     in case parse thy ct of

 		          *)

 		          *)

     (case is_known thy sel oris (term_of ct) of

     (case is_known thy sel oris (term_of ct) of

 	 (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);

 	 (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);

 	     *)

 	     *)

 	 ("",ori'(*ts='ct'*), all) => 

 	 ("",ori'(*ts='ct'*), all) => 

    *)

    *)

 fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';

 fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';

 fun fstr2itm_ thy pbt (f, str) =

 fun fstr2itm_ thy pbt (f, str) =

     let val topt = parse thy str

     let val topt = parse thy str

     in case topt of

     in case topt of

    *)

    *)

 	   let val (d,ts) = ((split_dts thy) o term_of) ct

 	   let val (d,ts) = ((split_dts thy) o term_of) ct

 	       val popt = find_first (eq7 (f,d)) pbt

 	       val popt = find_first (eq7 (f,d)) pbt

 	   in case popt of

 	   in case popt of

 	   end

 	   end

     end; 

     end; 

 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

 (*fo = ifo excluded already in inform*)

 (*fo = ifo excluded already in inform*)

 fun concat_deriv rew_ord erls rules fo ifo =

 fun concat_deriv rew_ord erls rules fo ifo =

     let fun derivat ([]:(term * rule * (term * term list)) list) = e_term

     let fun derivat ([]:(term * rule * (term * term list)) list) = e_term

 	  | derivat dt = (#1 o #3 o last_elem) dt

 	  | derivat dt = (#1 o #3 o last_elem) dt

         fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2

         fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2

     in case (fod, ifod) of

     in case (fod, ifod) of

 	   ([], []) => if fo = ifo then (true, [])

 	   ([], []) => if fo = ifo then (true, [])

 		       else (false, [])

 		       else (false, [])

 	 | (fod, []) => if derivat fod = ifo 

 	 | (fod, []) => if derivat fod = ifo 

 			then (true, fod) (*ifo is normal form*)

 			then (true, fod) (*ifo is normal form*)

 		    val cs' as (tacis, c'', ptp) = 

 		    val cs' as (tacis, c'', ptp) = 

 			case tacis of

 			case tacis of

 			    ((Subproblem _, _, _)::_) => 

 			    ((Subproblem _, _, _)::_) => 

 			    let val ptp as (pt, (p,_)) = all_modspec ptp

 			    let val ptp as (pt, (p,_)) = all_modspec ptp

 				val mI = get_obj g_metID pt p

 				val mI = get_obj g_metID pt p

 					e_istate ptp end

 					e_istate ptp end

 			  | _ => cs';

 			  | _ => cs';

 		in compare_step (tacis, c @ c' @ c'', ptp) ifo end

 		in compare_step (tacis, c @ c' @ c'', ptp) ifo end

     end;

     end;

 (* writeln (trtas2str der);

 (* writeln (trtas2str der);

    val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =

    val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =

        (([],[],(pt,p)), (encode ifo));

        (([],[],(pt,p)), (encode ifo));

    *)

    *)

 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =

 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =

     case parse (assoc_thy "Isac.thy") istr of

     case parse (assoc_thy "Isac.thy") istr of

 	let val ifo = term_of ifo

 	let val ifo = term_of ifo

 	    val fo = case p_ of Frm => get_obj g_form pt p

 	    val fo = case p_ of Frm => get_obj g_form pt p

 			      | Res => (fst o (get_obj g_result pt)) p

 			      | Res => (fst o (get_obj g_result pt)) p

 			      | _ => #3 (get_obj g_origin pt p)

 			      | _ => #3 (get_obj g_origin pt p)

 	in if fo = ifo

 	in if fo = ifo

 	   then ("same-formula", cs)

 	   then ("same-formula", cs)

 	   (*thus ctree not cut with replaceFormula!*)

 	   (*thus ctree not cut with replaceFormula!*)

 	   else case cas_input ifo of

 	   else case cas_input ifo of

 		    compare_step ([],[],(pt,

 		    compare_step ([],[],(pt,

 				     (*last step re-calc in compare_step TODO*)

 				     (*last step re-calc in compare_step TODO*)

 					 lev_back pos)) ifo

 					 lev_back pos)) ifo

 	end

 	end

 (*------------------------------------------------------------------(**)

 (*------------------------------------------------------------------(**)

 end

 end

 open inform; 

 open inform;