equal
deleted
inserted
replaced
1 (* Title: ProgLang/Auto_Prog |
1 (* Title: ProgLang/Auto_Prog |
2 Author: Walther Neuper, Aug.2019 |
2 Author: Walther Neuper, Aug.2019 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 |
6 theory Auto_Prog imports Program Prog_Tac Tactical begin |
6 theory Auto_Prog imports Prog_Tac Tactical begin |
7 |
7 |
8 text \<open>Abstract: |
8 text \<open>Abstract: |
9 The tactics Rewrite_Set* create ONE step in a calculation by application of usually |
9 The tactics Rewrite_Set* create ONE step in a calculation by application of usually |
10 MORE than one theorem (here called "rule"). |
10 MORE than one theorem (here called "rule"). |
11 However, students can request details of rewriting down to single applications of theorems. |
11 However, students can request details of rewriting down to single applications of theorems. |