src/HOLCF/One.thy
changeset 1479 21eb5e156d91
parent 1274 ea0668a1c0ba
child 2275 dbce3dce821a
     1.1 --- a/src/HOLCF/One.thy	Tue Feb 06 12:27:17 1996 +0100
     1.2 +++ b/src/HOLCF/One.thy	Tue Feb 06 12:42:31 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/one.thy
     1.5 +(*  Title:      HOLCF/one.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Franz Regensburger
     1.8 +    Author:     Franz Regensburger
     1.9      Copyright   1993 Technische Universitaet Muenchen
    1.10  
    1.11  Introduce atomic type one = (void)u
    1.12 @@ -23,17 +23,17 @@
    1.13  arities one :: pcpo
    1.14  
    1.15  consts
    1.16 -	abs_one		:: "(void)u -> one"
    1.17 -	rep_one		:: "one -> (void)u"
    1.18 -	one 		:: "one"
    1.19 -	one_when 	:: "'c -> one -> 'c"
    1.20 +        abs_one         :: "(void)u -> one"
    1.21 +        rep_one         :: "one -> (void)u"
    1.22 +        one             :: "one"
    1.23 +        one_when        :: "'c -> one -> 'c"
    1.24  
    1.25  rules
    1.26 -  abs_one_iso	"abs_one`(rep_one`u) = u"
    1.27 -  rep_one_iso	"rep_one`(abs_one`x) = x"
    1.28 +  abs_one_iso   "abs_one`(rep_one`u) = u"
    1.29 +  rep_one_iso   "rep_one`(abs_one`x) = x"
    1.30  
    1.31  defs
    1.32 -  one_def	"one == abs_one`(up`UU)"
    1.33 +  one_def       "one == abs_one`(up`UU)"
    1.34    one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
    1.35  
    1.36  translations