equal
deleted
inserted
replaced
95 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
95 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
96 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
96 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
97 ML_file "Frontend/messages.sml" |
97 ML_file "Frontend/messages.sml" |
98 ML_file "Frontend/states.sml" |
98 ML_file "Frontend/states.sml" |
99 ML_file "Frontend/interface.sml" |
99 ML_file "Frontend/interface.sml" |
|
100 ML_file "Frontend/use-cases.sml" |
100 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: |
101 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS: |
101 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
102 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*) |
102 ML_file "print_exn_G.sml" |
103 ML_file "print_exn_G.sml" |
103 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
104 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
104 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*} |
105 ML {*"%%%%%%%%%%%%%%%%% start Knowledge %%%%%%%%%%%%%%%%%%%%%%";*} |