isabelle: src/HOLCF/Holcfb.ML@4127499d9b52 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	1	(* Title: HOLCF/holcfb.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 892 diff changeset	3	Author: Franz Regensburger
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	4	Changed by: David von Oheimb
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	Copyright 1993 Technische Universitaet Muenchen
1675 36ba4da350c3 adapted several proofs oheimb parents: 1461 diff changeset	6	*)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	open Holcfb;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	(* Some lemmas in HOL.thy *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	13	(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
1832 79dd1433867c removed old version of LEAST operator oheimb parents: 1675 diff changeset	17	val classical3 = (notE RS notI); (* [\| ?P ==> ~ ?P1; ?P ==> ?P1 \|] ==> ~ ?P *)

author	wenzelm
	Fri, 13 Dec 1996 17:34:32 +0100
changeset 2383	4127499d9b52
parent 2275	dbce3dce821a
permissions	-rw-r--r--