equal
deleted
inserted
replaced
29 \<^medskip> |
29 \<^medskip> |
30 This manual is written for users familiar with Isabelle/Isar, but not |
30 This manual is written for users familiar with Isabelle/Isar, but not |
31 necessarily Isabelle/ML. It covers the usage of the @{command method} as |
31 necessarily Isabelle/ML. It covers the usage of the @{command method} as |
32 well as the @{method match} method, as well as discussing their integration |
32 well as the @{method match} method, as well as discussing their integration |
33 with existing Isar concepts such as @{command named_theorems}. |
33 with existing Isar concepts such as @{command named_theorems}. |
|
34 |
|
35 These commands are provided by theory @{theory "Eisbach"} (see |
|
36 \<^file>\<open>~~/src/HOL/Eisbach/Eisbach.thy\<close>): it needs to be imported by all Eisbach |
|
37 applications. Theory theory @{theory "Eisbach_Tools"} provides additional |
|
38 proof methods and attributes that are occasionally useful. |
34 \<close> |
39 \<close> |
35 |
40 |
36 end |
41 end |