src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml
changeset 59916 2c0c34b18050
parent 59905 5e9118030ed9
child 59917 e98d714cca1a
equal deleted inserted replaced
59915:ff89369b717f 59916:2c0c34b18050
   140        (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
   140        (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
   141 		  | _ => (indt i) ^ "<METHODS>\n" ^
   141 		  | _ => (indt i) ^ "<METHODS>\n" ^
   142 			 foldl op ^ ("", map (keref2xml (i+i) Specify.Met_) met) ^
   142 			 foldl op ^ ("", map (keref2xml (i+i) Specify.Met_) met) ^
   143 			 (indt i) ^ "</METHODS>\n") ^
   143 			 (indt i) ^ "</METHODS>\n") ^
   144        indt i ^ "<EVALPRECOND>\n" ^ 
   144        indt i ^ "<EVALPRECOND>\n" ^ 
   145        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
   145        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
   146        indt i ^ "</EVALPRECOND>\n" ^
   146        indt i ^ "</EVALPRECOND>\n" ^
   147        authors2xml i "MATHAUTHORS" mathauthors ^
   147        authors2xml i "MATHAUTHORS" mathauthors ^
   148        authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
   148        authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
   149        "</NODECONTENT>" : xml
   149        "</NODECONTENT>" : xml
   150     end;
   150     end;
   205        indt i ^ "<META> </META>\n" ^
   205        indt i ^ "<META> </META>\n" ^
   206        scr2xml i scr ^
   206        scr2xml i scr ^
   207        pattern2xml i ppc pre ^
   207        pattern2xml i ppc pre ^
   208        indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
   208        indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
   209        indt i ^ "<EVALPRECOND>\n" ^ 
   209        indt i ^ "<EVALPRECOND>\n" ^ 
   210        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
   210        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
   211        indt i ^ "</EVALPRECOND>\n" ^
   211        indt i ^ "</EVALPRECOND>\n" ^
   212        indt i ^ "<EVALCOND>\n"    ^ 
   212        indt i ^ "<EVALCOND>\n"    ^ 
   213        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' erls')) "Rulesets" erls'^
   213        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' erls')) "Rulesets" erls'^
   214        indt i ^ "</EVALCOND>\n" ^
   214        indt i ^ "</EVALCOND>\n" ^
   215        indt i ^ "<EVALLISTEXPR>\n"^ 
   215        indt i ^ "<EVALLISTEXPR>\n"^ 
   216        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' srls')) "Rulesets" srls'^
   216        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' srls')) "Rulesets" srls'^
   217        indt i ^ "</EVALLISTEXPR>\n" ^
   217        indt i ^ "</EVALLISTEXPR>\n" ^
   218        indt i ^ "<CHECKELEMENTWISE>\n" ^ 
   218        indt i ^ "<CHECKELEMENTWISE>\n" ^ 
   219        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' crls')) "Rulesets" crls'^
   219        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' crls')) "Rulesets" crls'^
   220        indt i ^ "</CHECKELEMENTWISE>\n" ^
   220        indt i ^ "</CHECKELEMENTWISE>\n" ^
   221        indt i ^ "<NORMALFORM>\n"  ^ 
   221        indt i ^ "<NORMALFORM>\n"  ^ 
   222        theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
   222        theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
   223        indt i ^ "</NORMALFORM>\n" ^
   223        indt i ^ "</NORMALFORM>\n" ^
   224        indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
   224        indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
   225        calcs2xmlOLD i calc ^
   225        calcs2xmlOLD i calc ^
   226        authors2xml i "MATHAUTHORS" mathauthors ^
   226        authors2xml i "MATHAUTHORS" mathauthors ^
   227        authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
   227        authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^