- Moved rewriting functions to meta_simplifier.ML
- dest_abs now also takes an optional variable name as an argument
- beta_conversion takes additional flag as an argument. Fully reduces
the term if set to true
Some tuning:
- tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive,
transitive, beta_conversion, abstract_rule
- combination: chktypes derives types of f and t from type of == instead
of using fastype_of
New primitives:
- eta_conversion
- incr_indexes: increment indexes in theorems
- cterm_incr_indexes: increment indexes in cterms
- cterm_match, cterm_first_order_match
- rename_boundvars
Isabelle's Object-Logics. Report 286.
This is the third of the Isabelle manuals. It covers Isabelle's built-in
object logics: first-order logic (FOL), Zermelo-Fraenkel set theory (ZF),
higher-order logic (HOL), the classical sequent calculus (LK), and
constructive type theory (CTT). The final chapter discusses how to define
new logics. This manual assumes familiarity with Report 280, Introduction
to Isabelle.