isabelle: src/HOL/W0/MiniML.ML@f60e3d2c81d3 (annotated)

2520 aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	1	(* Title: HOL/W0/MiniML.ML
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	2	ID: $Id$
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	5	*)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	6
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	7	open MiniML;
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	8
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	9	Addsimps has_type.intrs;
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	10	Addsimps [Un_upper1,Un_upper2];
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	11
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	12
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	13	(* has_type is closed w.r.t. substitution *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	14	goal MiniML.thy "!!a e t. a \|- e :: t ==> $s a \|- e :: $s t";
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	15	by (etac has_type.induct 1);
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	16	(* case VarI *)
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2520 diff changeset	17	by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	18	by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2520 diff changeset	19	by ( fast_tac (HOL_cs addIs [has_type.VarI] addss (simpset() delsimps [nth_map])) 1);
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	20	(* case AbsI *)
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 2520 diff changeset	21	by (asm_full_simp_tac (simpset() addsimps [app_subst_list]) 1);
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	22	(* case AppI *)
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	23	by (Asm_full_simp_tac 1);
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	24	qed "has_type_cl_sub";

author	oheimb
	Wed, 12 Nov 1997 18:58:50 +0100
changeset 4223	f60e3d2c81d3
parent 4089	96fba19bcbe2
child 5069	3ea049f7979d
permissions	-rw-r--r--