src/Tools/isac/Interpret/ctree.sml
branchdecompose-isar
changeset 41980 6ec461ac6c76
parent 41977 a3ce4017f41d
child 41982 90f65f1b6351
     1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Mon May 09 10:43:43 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Wed May 11 07:28:13 2011 +0200
     1.3 @@ -529,12 +529,10 @@
     1.4  type fmz = fmz_ * spec;
     1.5  val e_fmz = ([],e_spec);
     1.6  
     1.7 -(*tac_ is made from tac in applicable_in,
     1.8 -  and carries all data necessary for generate;*)
     1.9 +(* tac_ is made from tac in applicable_in,
    1.10 +  and carries all data necessary for generate *)
    1.11  datatype tac_ = 
    1.12 -(* datatype tac = *)
    1.13    Init_Proof' of ((cterm' list) * spec)
    1.14 -                (* ori list !: code specify -> applicable*)
    1.15  | Model_Problem' of pblID * 
    1.16  		    itm list *  (*the 'untouched' pbl*)
    1.17  		    itm list    (*the casually completed met*)