Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MiniML/MiniML.ML
author nipkow
Mon, 20 May 1996 18:41:55 +0200
changeset 1751 946efd210837
parent 1743 f7feaacd33d3
child 2031 03a843f0f447
permissions -rw-r--r--
Added thm I_complete_wrt_W to I. Added a few lemmas to Maybe and Type.

(* Title:     HOL/MiniML/MiniML.ML
   ID:        $Id$
   Author:    Dieter Nazareth and Tobias Nipkow
   Copyright  1995 TU Muenchen
*)

open MiniML;

Addsimps has_type.intrs;
Addsimps [Un_upper1,Un_upper2];


(* has_type is closed w.r.t. substitution *)
goal MiniML.thy "!!a e t. a |- e :: t ==> $s a |- e :: $s t";
by (etac has_type.induct 1);
(* case VarI *)
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
by (forw_inst_tac [("f1","$ s")] (nth_map RS sym) 1);
by( fast_tac (HOL_cs addIs [has_type.VarI] addss (!simpset delsimps [nth_map])) 1);
(* case AbsI *)
by (asm_full_simp_tac (!simpset addsimps [app_subst_list]) 1);
(* case AppI *)
by (Asm_full_simp_tac 1);
qed "has_type_cl_sub";
isabelle