isabelle: src/HOL/Option.ML@b3e39a2987c1 (annotated)

2019 b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	1	(* Title: Option.ML
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	2	ID: $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	3	Author: Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	4	Copyright 1996 TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	5
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	6	Derived rules
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	7	*)
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	8
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	9	open Option;
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	10
3344 b3e39a2987c1 Deleted option_case_tac because exhaust_tac performs a similar function. paulson parents: 3295 diff changeset	11	goal Option.thy "P(case opt of None => a \| Some(x) => b x) = \
b3e39a2987c1 Deleted option_case_tac because exhaust_tac performs a similar function. paulson parents: 3295 diff changeset	12	\ ((opt = None --> P a) & (!x. opt = Some x --> P(b x)))";
2019 b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	13	by (option.induct_tac "opt" 1);
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	14	by (Simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL nipkow parents: diff changeset	15	by (Asm_full_simp_tac 1);
3344 b3e39a2987c1 Deleted option_case_tac because exhaust_tac performs a similar function. paulson parents: 3295 diff changeset	16	qed "expand_option_case";

author	paulson
	Mon, 26 May 1997 12:40:51 +0200
changeset 3344	b3e39a2987c1
parent 3295	c9c99aa082fb
child 4032	4b1c69d8b767
permissions	-rw-r--r--