Library
  signature INTERACTIVE
  structure Interactive
is
#if defined(NEW_CM)
  $/basis.cm
#endif
  ../tomega/sources.cm
  ../lambda/sources.cm
  ../global/sources.cm
  ../names/sources.cm
  ../print/sources.cm
  ../index/sources.cm
  ../modes/sources.cm
  ../typecheck/sources.cm
  ../table/sources.cm
  ../subordinate/sources.cm
  ../solvers/sources.cm
  ../opsem/sources.cm
  ../trail/sources.cm
  (* ../order/sources.cm *)
  ../compile/sources.cm
  ../worldcheck/sources.cm
  ../formatter/sources.cm
  ../timing/sources.cm
  state.sig       (* central data structure for states *)
  state.fun       
  search.sig
  search.fun	
  data.sig
  data.fun
  fill.sig        (* Filling existentials *)
  fill.fun
  split.sig       (* Splitting assumptions *)
  split.fun
  fixedpoint.sig  (* Fixed point rule *)
  fixedpoint.fun 
(*   recurse.sig     (* Computing induction hypotheses *)
  recurse.fun	*)
  introduce.sig   (* Introduce assumptions in the context *)
  introduce.fun
  elim.sig        (* Elimination forms for meta level assumptions *)
  elim.fun
  interactive.sig
  interactive.fun
  weaken.sig
  weaken.fun
  prover.sml