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

48475 02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	1	session LCF! in "." = Pure +
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	2	description {*
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	3	Author: Tobias Nipkow
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	4	Copyright 1992 University of Cambridge
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	5	*}
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	6	theories LCF
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	7
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	8	session ex = LCF +
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	9	description {*
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	10	Author: Tobias Nipkow
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	Some examples from Lawrence Paulson's book Logic and Computation.
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	14	*}
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	15	theories Ex1 Ex2 Ex3 Ex4
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	16