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
```