isabelle: src/ZF/IMP/Assign.ML@9e66e8ed8237 (annotated)

482 3a4e092ba69c Initial revision nipkow parents: diff changeset	1	(* Title: ZF/IMP/Assign.ML
3a4e092ba69c Initial revision nipkow parents: diff changeset	2	ID: $Id$
3a4e092ba69c Initial revision nipkow parents: diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
3a4e092ba69c Initial revision nipkow parents: diff changeset	4	Copyright 1994 TUM
3a4e092ba69c Initial revision nipkow parents: diff changeset	5	*)
3a4e092ba69c Initial revision nipkow parents: diff changeset	6
3a4e092ba69c Initial revision nipkow parents: diff changeset	7	open Assign;
3a4e092ba69c Initial revision nipkow parents: diff changeset	8
3a4e092ba69c Initial revision nipkow parents: diff changeset	9	val assign_type = prove_goalw Assign.thy [assign_def]
3a4e092ba69c Initial revision nipkow parents: diff changeset	10	"[\| sigma:loc -> nat; n:nat \|] ==> sigma[n/x] : loc -> nat"
3a4e092ba69c Initial revision nipkow parents: diff changeset	11	(fn prems => [(fast_tac
3a4e092ba69c Initial revision nipkow parents: diff changeset	12	(ZF_cs addIs [apply_type,lam_type,if_type]@prems) 1)]);