Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
(* Title: HOL/MiniML/Generalize.thy
ID: $Id$
Author: Wolfgang Naraschewski and Tobias Nipkow
Copyright 1996 TU Muenchen
Generalizing type schemes with respect to a context
*)
Generalize = Instance +
(* gen: binding (generalising) the variables which are not free in the context *)
types ctxt = type_scheme list
consts
gen :: [ctxt, typ] => type_scheme
primrec
"gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
"gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
(* executable version of gen: Implementation with free_tv_ML *)
consts
gen_ML_aux :: [nat list, typ] => type_scheme
primrec
"gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
"gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
consts
gen_ML :: [ctxt, typ] => type_scheme
defs
gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
end