isabelle: src/HOL/IOA/meta_theory/Option.ML@3fd66f245ad7 (annotated)

966 3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	1	(* Title: Option.ML
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	2	ID: $Id$
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	4	Copyright 1994 TU Muenchen
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	5
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	6	Derived rules
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	7	*)
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	8
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	9	val option_rws = Let_def :: Option.option.simps;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	10	val SS = arith_ss addsimps option_rws;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	11
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	12	val [prem] = goal Option.thy "P(opt) ==> P(None) \| (? x. P(Some(x)))";
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	13	br (prem RS rev_mp) 1;
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	14	by (Option.option.induct_tac "opt" 1);
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	15	by (ALLGOALS(fast_tac HOL_cs));
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	16	val optE = store_thm("optE", standard(result() RS disjE));

author	clasohm
	Mon, 20 Mar 1995 15:37:03 +0100
changeset 966	3fd66f245ad7
child 1052	e044350bfa52
permissions	-rw-r--r--