src/ZF/Coind/Static.ML
author wenzelm
Sat, 27 Oct 2001 00:09:59 +0200
changeset 11963 a6608d44a46b
parent 6141 a6922171b396
permissions -rw-r--r--
impose hyps on initial goal configuration (prevents res_inst_tac problems);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 916
diff changeset
     1
(*  Title:      ZF/Coind/Static.ML
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 916
diff changeset
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     5
*)
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     6
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
     7
val elab_constE	= ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
     8
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
     9
val elab_varE 	= ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    10
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    11
val elab_fnE 	= ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    12
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    13
val elab_fixE 	= ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    14
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    15
val elab_appE 	= ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    16
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    17
AddSEs [elab_constE, elab_varE, elab_fixE];
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    18
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    19
AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
916
d03bb9f50b3b New example by Jacob Frost, tidied by lcp
lcp
parents:
diff changeset
    20
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    21
AddIs  [ElabRel.appI];
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    22
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    23
AddEs [elab_appE, elab_fnE];
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    24
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 4091
diff changeset
    25
AddDs [ElabRel.dom_subset RS subsetD];