equal
deleted
inserted
replaced
1 theory Tactical |
1 theory Tactical |
2 imports Base FirstSteps |
2 imports Base FirstSteps |
3 begin |
3 begin |
|
4 |
|
5 (*<*) |
|
6 setup{* |
|
7 open_file_with_prelude |
|
8 "Tactical_Code.thy" |
|
9 ["theory Tactical", "imports Base FirstSteps", "begin"] |
|
10 *} |
|
11 (*>*) |
4 |
12 |
5 chapter {* Tactical Reasoning\label{chp:tactical} *} |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
6 |
14 |
7 text {* |
15 text {* |
8 One of the main reason for descending to the ML-level of Isabelle is to be able to |
16 One of the main reason for descending to the ML-level of Isabelle is to be able to |