--- a/src/ZF/IMP/Aexp.ML Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: ZF/IMP/Aexp.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
- Copyright 1994 TUM
-*)
-
-structure Aexp = Datatype_Fun
- (
- val thy = Univ.thy |> add_consts [("loc", "i", NoSyn)]
- val thy_name = "Aexp"
- val rec_specs =
- [(
- "aexp", "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )",
- [
- (["N","X"], "i => i", NoSyn),
- (["Op1"], "[i,i] => i", NoSyn),
- (["Op2"], "[i,i,i] => i", NoSyn)
- ]
- )];
-
- val rec_styp = "i";
- val ext = None;
-
- val sintrs =
- [
- "n:nat ==> N(n) : aexp",
- "x:loc ==> X(x) : aexp",
- "[| f: nat -> nat; a : aexp |] ==> Op1(f,a) : aexp",
- "[| f: (nat * nat) -> nat; a0 : aexp; a1: aexp |] \
-\ ==> Op2(f,a0,a1) : aexp"
- ];
- val monos = [];
- val type_intrs = datatype_intrs;
- val type_elims = datatype_elims;
- );