equal
deleted
inserted
replaced
1 (* Title: collect all defitions for the program language |
1 (* Title: collect all defitions for the program language |
2 Author: Walther Neuper 100831 |
2 Author: Walther Neuper 100831 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 theory ProgLang imports Prog_Expr Auto_Prog |
5 theory ProgLang |
|
6 imports Prog_Expr Auto_Prog |
6 begin |
7 begin |
|
8 |
|
9 text \<open>Abstract: |
|
10 Here the language is defined, which extends Isabelle's functions to Isac's programs |
|
11 for Lucas-Interpretation. |
|
12 The language is interpreted by use of Isac's rewrite engine, defined in the ML-file below. |
|
13 \<close> |
7 |
14 |
8 ML_file rewrite.sml |
15 ML_file rewrite.sml |
9 |
16 |
10 ML \<open> |
17 ML \<open> |
11 \<close> ML \<open> |
18 \<close> ML \<open> |