equal
deleted
inserted
replaced
6 theory Specify |
6 theory Specify |
7 imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic" |
7 imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic" |
8 keywords "cas" :: thy_decl |
8 keywords "cas" :: thy_decl |
9 begin |
9 begin |
10 ML_file "o-model.sml" |
10 ML_file "o-model.sml" |
|
11 ML_file "pre-conditions.sml" (*uses Model_Def.i_model*) |
11 ML_file "i-model.sml" |
12 ML_file "i-model.sml" |
12 ML_file "pre-conditions.sml" |
|
13 ML_file "p-model.sml" |
13 ML_file "p-model.sml" |
14 ML_file "m-match.sml" |
14 ML_file "m-match.sml" |
15 ML_file refine.sml |
15 ML_file refine.sml |
16 ML_file "test-out.sml" |
16 ML_file "test-out.sml" |
17 ML_file "specify-step.sml" |
17 ML_file "specify-step.sml" |