isabelle: src/ZF/Coind/Language.thy@a901bafe4578 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Coind/Language.thy
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Jacob Frost, Cambridge University Computer Laboratory
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	5	*)
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	6
2874 b1e7e2179597 Datatype declarations now require theory Datatype--NOT in quotes paulson parents: 1478 diff changeset	7	Language = Datatype + QUniv +
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	8
932 b7ab04253326 Got rid of exvarU and constU by lcp parents: 915 diff changeset	9	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	10	Const :: i (* Abstract type of constants *)
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	11	c_app :: [i,i] => i (Abstract constructor for fun application)
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	12
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	13	rules
932 b7ab04253326 Got rid of exvarU and constU by lcp parents: 915 diff changeset	14	constNEE "c:Const ==> c ~= 0"
b7ab04253326 Got rid of exvarU and constU by lcp parents: 915 diff changeset	15	c_appI "[\| c1:Const; c2:Const \|] ==> c_app(c1,c2):Const"
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	16
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	17
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	18	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	19	Exp :: i (* Datatype of expressions *)
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	ExVar :: i (* Abstract type of variables *)
6112 5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	21
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	22	datatype
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	23	"Exp" = e_const ("c:Const")
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	24	\| e_var ("x:ExVar")
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	25	\| e_fn ("x:ExVar","e:Exp")
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	26	\| e_fix ("x1:ExVar","x2:ExVar","e:Exp")
5e4871c5136b datatype package improvements paulson parents: 2874 diff changeset	27	\| e_app ("e1:Exp","e2:Exp")
915 6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	28
6dae0daf57b7 New example by Jacob Frost, tidied by lcp lcp parents: diff changeset	29	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 6112	5e4871c5136b
child 11318	6536fb8c9fc6
permissions	-rw-r--r--