src/ZF/ex/Term.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/ex/Term.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ex/Term.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/ex/Term.thy
     1.5 +(*  Title:      ZF/ex/Term.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1994  University of Cambridge
    1.10  
    1.11  Terms over an alphabet.
    1.12 @@ -19,7 +19,7 @@
    1.13  
    1.14  datatype
    1.15    "term(A)" = Apply ("a: A", "l: list(term(A))")
    1.16 -  monos	      "[list_mono]"
    1.17 +  monos       "[list_mono]"
    1.18  
    1.19    type_elims  "[make_elim (list_univ RS subsetD)]"
    1.20  (*Or could have
    1.21 @@ -31,12 +31,12 @@
    1.22     "term_rec(t,d) == 
    1.23     Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
    1.24  
    1.25 -  term_map_def	"term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
    1.26 +  term_map_def  "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
    1.27  
    1.28 -  term_size_def	"term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
    1.29 +  term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
    1.30  
    1.31 -  reflect_def	"reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
    1.32 +  reflect_def   "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
    1.33  
    1.34 -  preorder_def	"preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
    1.35 +  preorder_def  "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
    1.36  
    1.37  end