src/ZF/Let.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 4879 58656c6a3551
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/Let
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
     5
1094
840554ac0451 Patterns can now be let-bound
lcp
parents: 1061
diff changeset
     6
Let expressions, and tuple pattern-matching (borrowed from HOL)
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
     7
*)
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
     8
1094
840554ac0451 Patterns can now be let-bound
lcp
parents: 1061
diff changeset
     9
Let = FOL +
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    10
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    11
types
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    12
  letbinds  letbind
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    13
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    14
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1094
diff changeset
    15
  Let           :: ['a, 'a => 'b] => 'b
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    16
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    17
syntax
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1094
diff changeset
    18
  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1094
diff changeset
    19
  ""            :: letbind => letbinds              ("_")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1094
diff changeset
    20
  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1094
diff changeset
    21
  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
1061
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    22
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    23
translations
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    24
  "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    25
  "let x = a in e"          == "Let(a, %x. e)"
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    26
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    27
defs
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    28
  Let_def       "Let(s, f) == f(s)"
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    29
8897213195c0 Definition of 'let' declarations, from HOL
lcp
parents:
diff changeset
    30
end