1(*:maxLineLen=78:*) 2 3theory Preface 4imports Base "HOL-Eisbach.Eisbach_Tools" 5begin 6 7text \<open> 8 \<^emph>\<open>Eisbach\<close> is a collection of tools which form the basis for defining new 9 proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought of as 10 a ``proof method language'', but is more precisely an infrastructure for 11 defining new proof methods out of existing ones. 12 13 The core functionality of Eisbach is provided by the Isar @{command method} 14 command. Here users may define new methods by combining existing ones with 15 the usual Isar syntax. These methods can be abstracted over terms, facts and 16 other methods, as one might expect in any higher-order functional language. 17 18 Additional functionality is provided by extending the space of methods and 19 attributes. The new @{method match} method allows for explicit control-flow, 20 by taking a match target and a list of pattern-method pairs. By using the 21 functionality provided by Eisbach, additional support methods can be easily 22 written. For example, the @{method catch} method, which provides basic 23 try-catch functionality, only requires a few lines of ML. 24 25 Eisbach is meant to allow users to write automation using only Isar syntax. 26 Traditionally proof methods have been written in Isabelle/ML, which poses a 27 high barrier-to-entry for many users. 28 29 \<^medskip> 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 32 well as the @{method match} method, as well as discussing their integration 33 with existing Isar concepts such as @{command named_theorems}. 34 35 These commands are provided by theory @{theory "HOL-Eisbach.Eisbach"}: it 36 needs to be imported by all Eisbach applications. Theory theory @{theory 37 "HOL-Eisbach.Eisbach_Tools"} provides additional proof methods and 38 attributes that are occasionally useful. 39\<close> 40 41end 42