isabelle: src/HOL/Subst/AList.ML@c69542757a4d (annotated)

3268 012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	1	(* Title: Subst/AList.ML
012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	3	Author: Martin Coen, Cambridge University Computer Laboratory
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	5
3268 012c43174664 Mostly cosmetic changes: updated headers, ID lines, etc. paulson parents: 3192 diff changeset	6	Association lists.
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	7	*)
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	8
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	9	open AList;
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	10
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	11	val prems = goal AList.thy
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	12	"[\| P([]); \
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 968 diff changeset	13	\ !!x y xs. P(xs) ==> P((x,y)#xs) \|] ==> P(l)";
3192 a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	14	by (induct_tac "l" 1);
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	15	by (split_all_tac 2);
a75558a4ed37 New version, modified by Konrad Slind and LCP for TFL paulson parents: 1465 diff changeset	16	by (REPEAT (ares_tac prems 1));
968 3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	17	qed "alist_induct";
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	18
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	19	(Perform induction on xs. )
3cdaa8724175 converted Subst with curried function application clasohm parents: diff changeset	20	fun alist_ind_tac a M =
9747 043098ba5098 introduced induct_thm_tac nipkow parents: 8874 diff changeset	21	EVERY [induct_thm_tac alist_induct a M,
1465 5d7a7e439cec expanded tabs clasohm parents: 1266 diff changeset	22	rename_last_tac a ["1"] (M+1)];

author	nipkow
	Mon, 16 Aug 2004 14:22:27 +0200
changeset 15131	c69542757a4d
parent 9747	043098ba5098
permissions	-rw-r--r--