isabelle: src/HOL/MiniML/Generalize.thy@b5b15bbca582 (annotated)

2525 477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	1	(* Title: HOL/MiniML/Generalize.thy
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	2	ID: $Id$
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	3	Author: Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	4	Copyright 1996 TU Muenchen
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	5
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	6	Generalizing type schemes with respect to a context
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	7	*)
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	8
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	9	Generalize = Instance +
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	10
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	11
2625 69c1b8a493de Some lemmas changed to valuesd narasche parents: 2525 diff changeset	12	(* gen: binding (generalising) the variables which are not free in the context *)
2525 477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	13
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	14	types ctxt = type_scheme list
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	15
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	16	consts
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	17	gen :: [ctxt, typ] => type_scheme
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	18
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 2625 diff changeset	19	primrec
2525 477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	20	"gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
2625 69c1b8a493de Some lemmas changed to valuesd narasche parents: 2525 diff changeset	21	"gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
2525 477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	22
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	23	(* executable version of gen: Implementation with free_tv_ML *)
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	24
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	25	consts
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	26	gen_ML_aux :: [nat list, typ] => type_scheme
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	27
5184 9b8547a9496a Adapted to new datatype package. berghofe parents: 2625 diff changeset	28	primrec
5518 654ead0ba4f7 re-added mem and list_all oheimb parents: 5184 diff changeset	29	"gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
2625 69c1b8a493de Some lemmas changed to valuesd narasche parents: 2525 diff changeset	30	"gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
2525 477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	31
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	32	consts
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	33	gen_ML :: [ctxt, typ] => type_scheme
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	34
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	35	defs
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	36	gen_ML_def "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	37
477c05586286 The new version of MiniML including "let". nipkow parents: diff changeset	38	end

author	wenzelm
	Thu, 24 Jan 2002 16:37:49 +0100
changeset 12844	b5b15bbca582
parent 5518	654ead0ba4f7
child 14422	b8da5f258b04
permissions	-rw-r--r--