author | clasohm |
Thu, 23 Mar 1995 15:39:13 +0100 | |
changeset 971 | f4815812665b |
parent 482 | 3a4e092ba69c |
permissions | -rw-r--r-- |
482 | 1 |
(* Title: ZF/IMP/Assign.ML |
2 |
ID: $Id$ |
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 |
Copyright 1994 TUM |
|
5 |
*) |
|
6 |
||
7 |
open Assign; |
|
8 |
||
9 |
val assign_type = prove_goalw Assign.thy [assign_def] |
|
10 |
"[| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat" |
|
11 |
(fn prems => [(fast_tac |
|
12 |
(ZF_cs addIs [apply_type,lam_type,if_type]@prems) 1)]); |