src/Pure/Interface/isamode.ML

- 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

(*  Title:      Pure/Interface/isamode.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Configuration for David Aspinall's Isamode.
*)

signature ISAMODE =
sig
  val setup: (theory -> theory) list
  val init: bool -> unit
end;

structure Isamode: ISAMODE =
struct

(** compile-time theory setup **)

(* token translations *)

val isamodeN = "Isamode";

local

val end_tag = "\^A0";
val tclass_tag = "\^A1";
val tfree_tag = "\^A2";
val tvar_tag = "\^A3";
val free_tag = "\^A4";
val bound_tag = "\^A5";
val var_tag = "\^A6";

fun tagit p x = (p ^ x ^ end_tag, real (size x));

in

val isamode_trans =
 Syntax.tokentrans_mode isamodeN
  [("class", tagit tclass_tag),
   ("tfree", tagit tfree_tag),
   ("tvar", tagit tvar_tag),
   ("free", tagit free_tag),
   ("bound", tagit bound_tag),
   ("var", tagit var_tag)];

end;


(* setup *)

val setup = [Theory.add_tokentrfuns isamode_trans];



(** run-time initialization **)

fun init isamode =
  if isamode then print_mode := [Symbol.isabelle_fontN, Symbol.symbolsN, isamodeN]
  else print_mode := [Symbol.isabelle_fontN, Symbol.symbolsN];


end;