isabelle: src/CTT/ROOT@02dd825f5a4e (annotated)

48475 02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	1	session CTT! in "." = Pure +
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	2	description {*
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	4	Copyright 1991 University of Cambridge
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	5	*}
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	6	theories Main
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	7
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	8	session ex = CTT +
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	9	description {*
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	10	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	11	Copyright 1991 University of Cambridge
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	12
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	13	Examples for Constructive Type Theory.
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	14	*}
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	15	theories Typechecking Elimination Equality Synthesis

author	wenzelm
	Tue, 24 Jul 2012 14:07:44 +0200
changeset 48475	02dd825f5a4e
child 48483	9bfb6978eb80
permissions	-rw-r--r--