expanded tabs
authorclasohm
Tue Feb 06 12:42:31 1996 +0100 (1996-02-06)
changeset 147921eb5e156d91
parent 1478 2b8c2a7547ab
child 1480 85ecd3439e01
expanded tabs
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.thy
src/HOLCF/Cfun3.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod1.thy
src/HOLCF/Cprod2.thy
src/HOLCF/Cprod3.thy
src/HOLCF/Fix.thy
src/HOLCF/Fun1.thy
src/HOLCF/Fun2.thy
src/HOLCF/Fun3.thy
src/HOLCF/HOLCF.thy
src/HOLCF/Holcfb.thy
src/HOLCF/Lift1.thy
src/HOLCF/Lift2.thy
src/HOLCF/Lift3.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Porder0.thy
src/HOLCF/Sprod0.thy
src/HOLCF/Sprod1.thy
src/HOLCF/Sprod2.thy
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum0.thy
src/HOLCF/Ssum1.thy
src/HOLCF/Ssum2.thy
src/HOLCF/Ssum3.thy
src/HOLCF/Tr1.thy
src/HOLCF/Tr2.thy
src/HOLCF/Void.thy
src/HOLCF/ccc1.thy
src/HOLCF/ex/Fix2.thy
src/HOLCF/ex/Hoare.thy
src/HOLCF/ex/Loop.thy
src/HOLCF/explicit_domains/Coind.thy
src/HOLCF/explicit_domains/Dagstuhl.thy
src/HOLCF/explicit_domains/Dlist.thy
src/HOLCF/explicit_domains/Dnat.thy
src/HOLCF/explicit_domains/Dnat2.thy
src/HOLCF/explicit_domains/Focus_ex.thy
src/HOLCF/explicit_domains/Stream.thy
src/HOLCF/explicit_domains/Stream2.thy
     1.1 --- a/src/HOLCF/Cfun1.thy	Tue Feb 06 12:27:17 1996 +0100
     1.2 +++ b/src/HOLCF/Cfun1.thy	Tue Feb 06 12:42:31 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/cfun1.thy
     1.5 +(*  Title:      HOLCF/cfun1.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  Definition of the type ->  of continuous functions
    1.12 @@ -14,38 +14,38 @@
    1.13  
    1.14  types "->" 2        (infixr 5)
    1.15  
    1.16 -arities "->" :: (pcpo,pcpo)term		(* No properties for ->'s range *)
    1.17 +arities "->" :: (pcpo,pcpo)term         (* No properties for ->'s range *)
    1.18  
    1.19  consts  
    1.20 -	Cfun	:: "('a => 'b)set"
    1.21 -	fapp	:: "('a -> 'b)=>('a => 'b)"	(* usually Rep_Cfun *)
    1.22 -						(* application      *)
    1.23 +        Cfun    :: "('a => 'b)set"
    1.24 +        fapp    :: "('a -> 'b)=>('a => 'b)"     (* usually Rep_Cfun *)
    1.25 +                                                (* application      *)
    1.26  
    1.27 -	fabs	:: "('a => 'b)=>('a -> 'b)"	(binder "LAM " 10)
    1.28 -						(* usually Abs_Cfun *)
    1.29 -						(* abstraction      *)
    1.30 +        fabs    :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    1.31 +                                                (* usually Abs_Cfun *)
    1.32 +                                                (* abstraction      *)
    1.33  
    1.34 -	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    1.35 +        less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    1.36  
    1.37  syntax  "@fapp"     :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
    1.38  
    1.39  translations "f`x" == "fapp f x"
    1.40  
    1.41  defs 
    1.42 -  Cfun_def	"Cfun == {f. cont(f)}"
    1.43 +  Cfun_def      "Cfun == {f. cont(f)}"
    1.44  
    1.45  rules
    1.46  
    1.47    (*faking a type definition... *)
    1.48    (* -> is isomorphic to Cfun   *)
    1.49  
    1.50 -  Rep_Cfun		"fapp fo : Cfun"
    1.51 -  Rep_Cfun_inverse	"fabs (fapp fo) = fo"
    1.52 -  Abs_Cfun_inverse	"f:Cfun ==> fapp(fabs f) = f"
    1.53 +  Rep_Cfun              "fapp fo : Cfun"
    1.54 +  Rep_Cfun_inverse      "fabs (fapp fo) = fo"
    1.55 +  Abs_Cfun_inverse      "f:Cfun ==> fapp(fabs f) = f"
    1.56  
    1.57  defs
    1.58    (*defining the abstract constants*)
    1.59 -  less_cfun_def		"less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
    1.60 +  less_cfun_def         "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
    1.61  
    1.62  (* start 8bit 1 *)
    1.63  (* end 8bit 1 *)
     2.1 --- a/src/HOLCF/Cfun2.thy	Tue Feb 06 12:27:17 1996 +0100
     2.2 +++ b/src/HOLCF/Cfun2.thy	Tue Feb 06 12:42:31 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	HOLCF/cfun2.thy
     2.5 +(*  Title:      HOLCF/cfun2.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Franz Regensburger
     2.8 +    Author:     Franz Regensburger
     2.9      Copyright   1993 Technische Universitaet Muenchen
    2.10  
    2.11  Class Instance ->::(pcpo,pcpo)po
    2.12 @@ -12,19 +12,19 @@
    2.13  (* Witness for the above arity axiom is cfun1.ML *)
    2.14  arities "->" :: (pcpo,pcpo)po
    2.15  
    2.16 -consts	
    2.17 -	UU_cfun  :: "'a->'b"
    2.18 +consts  
    2.19 +        UU_cfun  :: "'a->'b"
    2.20  
    2.21  rules
    2.22  
    2.23  (* instance of << for type ['a -> 'b]  *)
    2.24  
    2.25 -inst_cfun_po	"((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
    2.26 +inst_cfun_po    "((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
    2.27  
    2.28  defs
    2.29  (* The least element in type 'a->'b *)
    2.30  
    2.31 -UU_cfun_def	"UU_cfun == fabs(% x.UU)"
    2.32 +UU_cfun_def     "UU_cfun == fabs(% x.UU)"
    2.33  
    2.34  end
    2.35  
     3.1 --- a/src/HOLCF/Cfun3.thy	Tue Feb 06 12:27:17 1996 +0100
     3.2 +++ b/src/HOLCF/Cfun3.thy	Tue Feb 06 12:42:31 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	HOLCF/cfun3.thy
     3.5 +(*  Title:      HOLCF/cfun3.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Franz Regensburger
     3.8 +    Author:     Franz Regensburger
     3.9      Copyright   1993 Technische Universitaet Muenchen
    3.10  
    3.11  Class instance of  -> for class pcpo
    3.12 @@ -9,21 +9,21 @@
    3.13  
    3.14  Cfun3 = Cfun2 +
    3.15  
    3.16 -arities "->"	:: (pcpo,pcpo)pcpo		(* Witness cfun2.ML *)
    3.17 +arities "->"    :: (pcpo,pcpo)pcpo              (* Witness cfun2.ML *)
    3.18  
    3.19  consts  
    3.20 -	Istrictify   :: "('a->'b)=>'a=>'b"
    3.21 -	strictify    :: "('a->'b)->'a->'b"
    3.22 +        Istrictify   :: "('a->'b)=>'a=>'b"
    3.23 +        strictify    :: "('a->'b)->'a->'b"
    3.24  
    3.25  rules 
    3.26  
    3.27 -inst_cfun_pcpo	"(UU::'a->'b) = UU_cfun"
    3.28 +inst_cfun_pcpo  "(UU::'a->'b) = UU_cfun"
    3.29  
    3.30  defs
    3.31  
    3.32 -Istrictify_def	"Istrictify f x == if x=UU then UU else f`x"	
    3.33 +Istrictify_def  "Istrictify f x == if x=UU then UU else f`x"    
    3.34  
    3.35 -strictify_def	"strictify == (LAM f x.Istrictify f x)"
    3.36 +strictify_def   "strictify == (LAM f x.Istrictify f x)"
    3.37  
    3.38  end
    3.39  
     4.1 --- a/src/HOLCF/Cont.thy	Tue Feb 06 12:27:17 1996 +0100
     4.2 +++ b/src/HOLCF/Cont.thy	Tue Feb 06 12:42:31 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	HOLCF/cont.thy
     4.5 +(*  Title:      HOLCF/cont.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Franz Regensburger
     4.8 +    Author:     Franz Regensburger
     4.9      Copyright   1993 Technische Universitaet Muenchen
    4.10  
    4.11      Results about continuity and monotonicity
    4.12 @@ -19,19 +19,19 @@
    4.13  default pcpo
    4.14  
    4.15  consts  
    4.16 -	monofun :: "('a::po => 'b::po) => bool"	(* monotonicity    *)
    4.17 -	contlub	:: "('a => 'b) => bool"		(* first cont. def *)
    4.18 -	cont	:: "('a => 'b) => bool"		(* secnd cont. def *)
    4.19 +        monofun :: "('a::po => 'b::po) => bool" (* monotonicity    *)
    4.20 +        contlub :: "('a => 'b) => bool"         (* first cont. def *)
    4.21 +        cont    :: "('a => 'b) => bool"         (* secnd cont. def *)
    4.22  
    4.23  defs 
    4.24  
    4.25 -monofun		"monofun(f) == ! x y. x << y --> f(x) << f(y)"
    4.26 +monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
    4.27  
    4.28 -contlub		"contlub(f) == ! Y. is_chain(Y) --> 
    4.29 -				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
    4.30 +contlub         "contlub(f) == ! Y. is_chain(Y) --> 
    4.31 +                                f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
    4.32  
    4.33 -cont		"cont(f)   == ! Y. is_chain(Y) --> 
    4.34 -				range(% i.f(Y(i))) <<| f(lub(range(Y)))"
    4.35 +cont            "cont(f)   == ! Y. is_chain(Y) --> 
    4.36 +                                range(% i.f(Y(i))) <<| f(lub(range(Y)))"
    4.37  
    4.38  (* ------------------------------------------------------------------------ *)
    4.39  (* the main purpose of cont.thy is to show:                                 *)
     5.1 --- a/src/HOLCF/Cprod1.thy	Tue Feb 06 12:27:17 1996 +0100
     5.2 +++ b/src/HOLCF/Cprod1.thy	Tue Feb 06 12:42:31 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title: 	HOLCF/cprod1.thy
     5.5 +(*  Title:      HOLCF/cprod1.thy
     5.6      ID:         $Id$
     5.7 -    Author: 	Franz Regensburger
     5.8 +    Author:     Franz Regensburger
     5.9      Copyright   1993  Technische Universitaet Muenchen
    5.10  
    5.11  
    5.12 @@ -12,12 +12,12 @@
    5.13  
    5.14  
    5.15  consts
    5.16 -  less_cprod	:: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"	
    5.17 +  less_cprod    :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"  
    5.18  
    5.19  defs
    5.20  
    5.21    less_cprod_def "less_cprod p1 p2 == ( fst(p1) << fst(p2) &
    5.22 -					snd(p1) << snd(p2))"
    5.23 +                                        snd(p1) << snd(p2))"
    5.24  
    5.25  end
    5.26  
     6.1 --- a/src/HOLCF/Cprod2.thy	Tue Feb 06 12:27:17 1996 +0100
     6.2 +++ b/src/HOLCF/Cprod2.thy	Tue Feb 06 12:42:31 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title: 	HOLCF/cprod2.thy
     6.5 +(*  Title:      HOLCF/cprod2.thy
     6.6      ID:         $Id$
     6.7 -    Author: 	Franz Regensburger
     6.8 +    Author:     Franz Regensburger
     6.9      Copyright   1993 Technische Universitaet Muenchen
    6.10  
    6.11  Class Instance *::(pcpo,pcpo)po
    6.12 @@ -17,7 +17,7 @@
    6.13  
    6.14  (* instance of << for type ['a * 'b]  *)
    6.15  
    6.16 -inst_cprod_po	"((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
    6.17 +inst_cprod_po   "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
    6.18  
    6.19  end
    6.20  
     7.1 --- a/src/HOLCF/Cprod3.thy	Tue Feb 06 12:27:17 1996 +0100
     7.2 +++ b/src/HOLCF/Cprod3.thy	Tue Feb 06 12:42:31 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title: 	HOLCF/cprod3.thy
     7.5 +(*  Title:      HOLCF/cprod3.thy
     7.6      ID:         $Id$
     7.7 -    Author: 	Franz Regensburger
     7.8 +    Author:     Franz Regensburger
     7.9      Copyright   1993 Technische Universitaet Muenchen
    7.10  
    7.11  
    7.12 @@ -10,31 +10,31 @@
    7.13  
    7.14  Cprod3 = Cprod2 +
    7.15  
    7.16 -arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)
    7.17 +arities "*" :: (pcpo,pcpo)pcpo                  (* Witness cprod2.ML *)
    7.18  
    7.19  consts  
    7.20 -	cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
    7.21 -	cfst         :: "('a*'b)->'a"
    7.22 -	csnd         :: "('a*'b)->'b"
    7.23 -	csplit       :: "('a->'b->'c)->('a*'b)->'c"
    7.24 +        cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
    7.25 +        cfst         :: "('a*'b)->'a"
    7.26 +        csnd         :: "('a*'b)->'b"
    7.27 +        csplit       :: "('a->'b->'c)->('a*'b)->'c"
    7.28  
    7.29 -syntax	
    7.30 -	"@ctuple"    :: "['a, args] => 'a * 'b"		("(1<_,/ _>)")
    7.31 +syntax  
    7.32 +        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
    7.33  
    7.34  
    7.35  translations 
    7.36 -	"<x, y, z>"   == "<x, <y, z>>"
    7.37 -	"<x, y>"      == "cpair`x`y"
    7.38 +        "<x, y, z>"   == "<x, <y, z>>"
    7.39 +        "<x, y>"      == "cpair`x`y"
    7.40  
    7.41  rules 
    7.42  
    7.43 -inst_cprod_pcpo	"(UU::'a*'b) = (UU,UU)"
    7.44 +inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
    7.45  
    7.46  defs
    7.47 -cpair_def	"cpair  == (LAM x y.(x,y))"
    7.48 -cfst_def	"cfst   == (LAM p.fst(p))"
    7.49 -csnd_def	"csnd   == (LAM p.snd(p))"	
    7.50 -csplit_def	"csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
    7.51 +cpair_def       "cpair  == (LAM x y.(x,y))"
    7.52 +cfst_def        "cfst   == (LAM p.fst(p))"
    7.53 +csnd_def        "csnd   == (LAM p.snd(p))"      
    7.54 +csplit_def      "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
    7.55  
    7.56  
    7.57  
     8.1 --- a/src/HOLCF/Fix.thy	Tue Feb 06 12:27:17 1996 +0100
     8.2 +++ b/src/HOLCF/Fix.thy	Tue Feb 06 12:42:31 1996 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4 -(*  Title: 	HOLCF/fix.thy
     8.5 +(*  Title:      HOLCF/fix.thy
     8.6      ID:         $Id$
     8.7 -    Author: 	Franz Regensburger
     8.8 +    Author:     Franz Regensburger
     8.9      Copyright   1993  Technische Universitaet Muenchen
    8.10  
    8.11  
    8.12 @@ -30,7 +30,7 @@
    8.13                          (!i.P(Y i)) --> P(lub(range Y))"
    8.14  
    8.15  admw_def      "admw P == !F. (!n.P (iterate n F UU)) -->
    8.16 -			    P (lub(range (%i. iterate i F UU)))" 
    8.17 +                            P (lub(range (%i. iterate i F UU)))" 
    8.18  
    8.19  chain_finite_def  "chain_finite (x::'a)==
    8.20                          !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
     9.1 --- a/src/HOLCF/Fun1.thy	Tue Feb 06 12:27:17 1996 +0100
     9.2 +++ b/src/HOLCF/Fun1.thy	Tue Feb 06 12:42:31 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title: 	HOLCF/fun1.thy
     9.5 +(*  Title:      HOLCF/fun1.thy
     9.6      ID:         $Id$
     9.7 -    Author: 	Franz Regensburger
     9.8 +    Author:     Franz Regensburger
     9.9      Copyright   1993  Technische Universitaet Muenchen
    9.10  
    9.11  
    9.12 @@ -15,7 +15,7 @@
    9.13  (* default class is still term *)
    9.14  
    9.15  consts
    9.16 -  less_fun	:: "['a=>'b::po,'a=>'b] => bool"	
    9.17 +  less_fun      :: "['a=>'b::po,'a=>'b] => bool"        
    9.18  
    9.19  defs
    9.20     (* definition of the ordering less_fun            *)
    10.1 --- a/src/HOLCF/Fun2.thy	Tue Feb 06 12:27:17 1996 +0100
    10.2 +++ b/src/HOLCF/Fun2.thy	Tue Feb 06 12:42:31 1996 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4 -(*  Title: 	HOLCF/fun2.thy
    10.5 +(*  Title:      HOLCF/fun2.thy
    10.6      ID:         $Id$
    10.7 -    Author: 	Franz Regensburger
    10.8 +    Author:     Franz Regensburger
    10.9      Copyright   1993 Technische Universitaet Muenchen
   10.10  
   10.11  Class Instance =>::(term,po)po
   10.12 @@ -15,20 +15,20 @@
   10.13  
   10.14  arities fun :: (term,po)po
   10.15  
   10.16 -consts	
   10.17 -	UU_fun  :: "'a::term => 'b::pcpo"
   10.18 +consts  
   10.19 +        UU_fun  :: "'a::term => 'b::pcpo"
   10.20  
   10.21  rules
   10.22  
   10.23  (* instance of << for type ['a::term => 'b::po]  *)
   10.24  
   10.25 -inst_fun_po	"((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
   10.26 +inst_fun_po     "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
   10.27  
   10.28  defs
   10.29  
   10.30  (* The least element in type 'a::term => 'b::pcpo *)
   10.31  
   10.32 -UU_fun_def	"UU_fun == (% x.UU)"
   10.33 +UU_fun_def      "UU_fun == (% x.UU)"
   10.34  
   10.35  end
   10.36  
    11.1 --- a/src/HOLCF/Fun3.thy	Tue Feb 06 12:27:17 1996 +0100
    11.2 +++ b/src/HOLCF/Fun3.thy	Tue Feb 06 12:42:31 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title: 	HOLCF/fun3.thy
    11.5 +(*  Title:      HOLCF/fun3.thy
    11.6      ID:         $Id$
    11.7 -    Author: 	Franz Regensburger
    11.8 +    Author:     Franz Regensburger
    11.9      Copyright   1993 Technische Universitaet Muenchen
   11.10  
   11.11  Class instance of  => (fun) for class pcpo
   11.12 @@ -11,11 +11,11 @@
   11.13  
   11.14  (* default class is still term *)
   11.15  
   11.16 -arities fun  :: (term,pcpo)pcpo		(* Witness fun2.ML *)
   11.17 +arities fun  :: (term,pcpo)pcpo         (* Witness fun2.ML *)
   11.18  
   11.19  rules 
   11.20  
   11.21 -inst_fun_pcpo	"(UU::'a=>'b::pcpo) = UU_fun"
   11.22 +inst_fun_pcpo   "(UU::'a=>'b::pcpo) = UU_fun"
   11.23  
   11.24  end
   11.25  
    12.1 --- a/src/HOLCF/HOLCF.thy	Tue Feb 06 12:27:17 1996 +0100
    12.2 +++ b/src/HOLCF/HOLCF.thy	Tue Feb 06 12:42:31 1996 +0100
    12.3 @@ -1,6 +1,6 @@
    12.4 -(*  Title: 	HOLCF/HOLCF.thy
    12.5 +(*  Title:      HOLCF/HOLCF.thy
    12.6      ID:         $Id$
    12.7 -    Author: 	Franz Regensburger
    12.8 +    Author:     Franz Regensburger
    12.9      Copyright   1993 Technische Universitaet Muenchen
   12.10  
   12.11  
    13.1 --- a/src/HOLCF/Holcfb.thy	Tue Feb 06 12:27:17 1996 +0100
    13.2 +++ b/src/HOLCF/Holcfb.thy	Tue Feb 06 12:42:31 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title: 	HOLCF/holcfb.thy
    13.5 +(*  Title:      HOLCF/holcfb.thy
    13.6      ID:         $Id$
    13.7 -    Author: 	Franz Regensburger
    13.8 +    Author:     Franz Regensburger
    13.9      Copyright   1993  Technische Universitaet Muenchen
   13.10  
   13.11  Basic definitions for the embedding of LCF into HOL.
   13.12 @@ -10,7 +10,7 @@
   13.13  Holcfb = Nat + 
   13.14  
   13.15  consts
   13.16 -	theleast     :: "(nat=>bool)=>nat"
   13.17 +        theleast     :: "(nat=>bool)=>nat"
   13.18  defs
   13.19  
   13.20  theleast_def    "theleast P == (@z.(P z & (!n.P n --> z<=n)))"
    14.1 --- a/src/HOLCF/Lift1.thy	Tue Feb 06 12:27:17 1996 +0100
    14.2 +++ b/src/HOLCF/Lift1.thy	Tue Feb 06 12:42:31 1996 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4 -(*  Title: 	HOLCF/Lift1.thy
    14.5 +(*  Title:      HOLCF/Lift1.thy
    14.6      ID:         $Id$
    14.7 -    Author: 	Franz Regensburger
    14.8 +    Author:     Franz Regensburger
    14.9      Copyright   1993  Technische Universitaet Muenchen
   14.10  
   14.11  
   14.12 @@ -14,12 +14,12 @@
   14.13  
   14.14  types "u" 1
   14.15  
   14.16 -arities "u" :: (pcpo)term	
   14.17 +arities "u" :: (pcpo)term       
   14.18  
   14.19  consts
   14.20  
   14.21 -  Rep_Lift	:: "('a)u => (void + 'a)"
   14.22 -  Abs_Lift	:: "(void + 'a) => ('a)u"
   14.23 +  Rep_Lift      :: "('a)u => (void + 'a)"
   14.24 +  Abs_Lift      :: "(void + 'a) => ('a)u"
   14.25  
   14.26    Iup           :: "'a => ('a)u"
   14.27    UU_lift       :: "('a)u"
   14.28 @@ -31,8 +31,8 @@
   14.29    (*faking a type definition... *)
   14.30    (* ('a)u is isomorphic to void + 'a  *)
   14.31  
   14.32 -  Rep_Lift_inverse	"Abs_Lift(Rep_Lift(p)) = p"	
   14.33 -  Abs_Lift_inverse	"Rep_Lift(Abs_Lift(p)) = p"
   14.34 +  Rep_Lift_inverse      "Abs_Lift(Rep_Lift(p)) = p"     
   14.35 +  Abs_Lift_inverse      "Rep_Lift(Abs_Lift(p)) = p"
   14.36  
   14.37     (*defining the abstract constants*)
   14.38  
   14.39 @@ -43,11 +43,11 @@
   14.40    Ilift_def     "Ilift(f)(x)== 
   14.41                  case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f`z"
   14.42   
   14.43 -  less_lift_def "less_lift(x1)(x2) == 		
   14.44 -          (case Rep_Lift(x1) of 		
   14.45 -               Inl(y1) => True 		
   14.46 -             | Inr(y2) => 			
   14.47 -                   (case Rep_Lift(x2) of Inl(z1) => False	
   14.48 +  less_lift_def "less_lift(x1)(x2) ==           
   14.49 +          (case Rep_Lift(x1) of                 
   14.50 +               Inl(y1) => True          
   14.51 +             | Inr(y2) =>                       
   14.52 +                   (case Rep_Lift(x2) of Inl(z1) => False       
   14.53                                         | Inr(z2) => y2<<z2))"
   14.54  
   14.55  end
    15.1 --- a/src/HOLCF/Lift2.thy	Tue Feb 06 12:27:17 1996 +0100
    15.2 +++ b/src/HOLCF/Lift2.thy	Tue Feb 06 12:42:31 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4 -(*  Title: 	HOLCF/lift2.thy
    15.5 +(*  Title:      HOLCF/lift2.thy
    15.6      ID:         $Id$
    15.7 -    Author: 	Franz Regensburger
    15.8 +    Author:     Franz Regensburger
    15.9      Copyright   1993 Technische Universitaet Muenchen
   15.10  
   15.11  Class Instance u::(pcpo)po
   15.12 @@ -17,7 +17,7 @@
   15.13  
   15.14  (* instance of << for type ('a)u  *)
   15.15  
   15.16 -inst_lift_po	"((op <<)::[('a)u,('a)u]=>bool) = less_lift"
   15.17 +inst_lift_po    "((op <<)::[('a)u,('a)u]=>bool) = less_lift"
   15.18  
   15.19  end
   15.20  
    16.1 --- a/src/HOLCF/Lift3.thy	Tue Feb 06 12:27:17 1996 +0100
    16.2 +++ b/src/HOLCF/Lift3.thy	Tue Feb 06 12:42:31 1996 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title: 	HOLCF/lift3.thy
    16.5 +(*  Title:      HOLCF/lift3.thy
    16.6      ID:         $Id$
    16.7 -    Author: 	Franz Regensburger
    16.8 +    Author:     Franz Regensburger
    16.9      Copyright   1993 Technische Universitaet Muenchen
   16.10  
   16.11  
   16.12 @@ -10,19 +10,19 @@
   16.13  
   16.14  Lift3 = Lift2 +
   16.15  
   16.16 -arities "u" :: (pcpo)pcpo			(* Witness lift2.ML *)
   16.17 +arities "u" :: (pcpo)pcpo                       (* Witness lift2.ML *)
   16.18  
   16.19  consts  
   16.20 -	up	     :: "'a -> ('a)u" 
   16.21 -	lift         :: "('a->'c)-> ('a)u -> 'c"
   16.22 +        up           :: "'a -> ('a)u" 
   16.23 +        lift         :: "('a->'c)-> ('a)u -> 'c"
   16.24  
   16.25  rules 
   16.26  
   16.27 -	inst_lift_pcpo	"(UU::('a)u) = UU_lift"
   16.28 +        inst_lift_pcpo  "(UU::('a)u) = UU_lift"
   16.29  
   16.30  defs
   16.31 -	up_def		"up     == (LAM x.Iup(x))"
   16.32 -	lift_def	"lift   == (LAM f p.Ilift(f)(p))"
   16.33 +        up_def          "up     == (LAM x.Iup(x))"
   16.34 +        lift_def        "lift   == (LAM f p.Ilift(f)(p))"
   16.35  
   16.36  translations
   16.37  "case l of up`x => t1" == "lift`(LAM x.t1)`l"
    17.1 --- a/src/HOLCF/One.thy	Tue Feb 06 12:27:17 1996 +0100
    17.2 +++ b/src/HOLCF/One.thy	Tue Feb 06 12:42:31 1996 +0100
    17.3 @@ -1,6 +1,6 @@
    17.4 -(*  Title: 	HOLCF/one.thy
    17.5 +(*  Title:      HOLCF/one.thy
    17.6      ID:         $Id$
    17.7 -    Author: 	Franz Regensburger
    17.8 +    Author:     Franz Regensburger
    17.9      Copyright   1993 Technische Universitaet Muenchen
   17.10  
   17.11  Introduce atomic type one = (void)u
   17.12 @@ -23,17 +23,17 @@
   17.13  arities one :: pcpo
   17.14  
   17.15  consts
   17.16 -	abs_one		:: "(void)u -> one"
   17.17 -	rep_one		:: "one -> (void)u"
   17.18 -	one 		:: "one"
   17.19 -	one_when 	:: "'c -> one -> 'c"
   17.20 +        abs_one         :: "(void)u -> one"
   17.21 +        rep_one         :: "one -> (void)u"
   17.22 +        one             :: "one"
   17.23 +        one_when        :: "'c -> one -> 'c"
   17.24  
   17.25  rules
   17.26 -  abs_one_iso	"abs_one`(rep_one`u) = u"
   17.27 -  rep_one_iso	"rep_one`(abs_one`x) = x"
   17.28 +  abs_one_iso   "abs_one`(rep_one`u) = u"
   17.29 +  rep_one_iso   "rep_one`(abs_one`x) = x"
   17.30  
   17.31  defs
   17.32 -  one_def	"one == abs_one`(up`UU)"
   17.33 +  one_def       "one == abs_one`(up`UU)"
   17.34    one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
   17.35  
   17.36  translations
    18.1 --- a/src/HOLCF/Pcpo.thy	Tue Feb 06 12:27:17 1996 +0100
    18.2 +++ b/src/HOLCF/Pcpo.thy	Tue Feb 06 12:42:31 1996 +0100
    18.3 @@ -3,15 +3,15 @@
    18.4  classes pcpo < po
    18.5  arities void :: pcpo
    18.6  
    18.7 -consts	
    18.8 -	UU :: "'a::pcpo"	
    18.9 +consts  
   18.10 +        UU :: "'a::pcpo"        
   18.11  
   18.12  rules
   18.13  
   18.14 -	minimal	"UU << x"	
   18.15 -	cpo	"is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" 
   18.16 +        minimal "UU << x"       
   18.17 +        cpo     "is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" 
   18.18  
   18.19 -inst_void_pcpo	"(UU::void) = UU_void"
   18.20 +inst_void_pcpo  "(UU::void) = UU_void"
   18.21  
   18.22  (* start 8bit 1 *)
   18.23  (* end 8bit 1 *)
    19.1 --- a/src/HOLCF/Porder.thy	Tue Feb 06 12:27:17 1996 +0100
    19.2 +++ b/src/HOLCF/Porder.thy	Tue Feb 06 12:42:31 1996 +0100
    19.3 @@ -1,6 +1,6 @@
    19.4 -(*  Title: 	HOLCF/porder.thy
    19.5 +(*  Title:      HOLCF/porder.thy
    19.6      ID:         $Id$
    19.7 -    Author: 	Franz Regensburger
    19.8 +    Author:     Franz Regensburger
    19.9      Copyright   1993 Technische Universitaet Muenchen
   19.10  
   19.11  Conservative extension of theory Porder0 by constant definitions 
   19.12 @@ -9,28 +9,28 @@
   19.13  
   19.14  Porder = Porder0 +
   19.15  
   19.16 -consts	
   19.17 -	"<|"	::	"['a set,'a::po] => bool"	(infixl 55)
   19.18 -	"<<|"	::	"['a set,'a::po] => bool"	(infixl 55)
   19.19 -	lub	::	"'a set => 'a::po"
   19.20 -	is_tord	::	"'a::po set => bool"
   19.21 -	is_chain ::	"(nat=>'a::po) => bool"
   19.22 -	max_in_chain :: "[nat,nat=>'a::po]=>bool"
   19.23 -	finite_chain :: "(nat=>'a::po)=>bool"
   19.24 +consts  
   19.25 +        "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)
   19.26 +        "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)
   19.27 +        lub     ::      "'a set => 'a::po"
   19.28 +        is_tord ::      "'a::po set => bool"
   19.29 +        is_chain ::     "(nat=>'a::po) => bool"
   19.30 +        max_in_chain :: "[nat,nat=>'a::po]=>bool"
   19.31 +        finite_chain :: "(nat=>'a::po)=>bool"
   19.32  
   19.33  defs
   19.34  
   19.35  (* class definitions *)
   19.36  
   19.37 -is_ub		"S  <| x == ! y.y:S --> y<<x"
   19.38 -is_lub		"S <<| x == S <| x & (! u. S <| u  --> x << u)"
   19.39 +is_ub           "S  <| x == ! y.y:S --> y<<x"
   19.40 +is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"
   19.41  
   19.42  
   19.43  (* Arbitrary chains are total orders    *)                  
   19.44 -is_tord		"is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
   19.45 +is_tord         "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
   19.46  
   19.47  (* Here we use countable chains and I prefer to code them as functions! *)
   19.48 -is_chain	"is_chain(F) == (! i.F(i) << F(Suc(i)))"
   19.49 +is_chain        "is_chain(F) == (! i.F(i) << F(Suc(i)))"
   19.50  
   19.51  (* finite chains, needed for monotony of continouous functions *)
   19.52  
   19.53 @@ -40,7 +40,7 @@
   19.54  
   19.55  rules
   19.56  
   19.57 -lub		"lub(S) = (@x. S <<| x)"
   19.58 +lub             "lub(S) = (@x. S <<| x)"
   19.59  
   19.60  (* start 8bit 1 *)
   19.61  (* end 8bit 1 *)
    20.1 --- a/src/HOLCF/Porder0.thy	Tue Feb 06 12:27:17 1996 +0100
    20.2 +++ b/src/HOLCF/Porder0.thy	Tue Feb 06 12:42:31 1996 +0100
    20.3 @@ -1,6 +1,6 @@
    20.4 -(*  Title: 	HOLCF/porder0.thy
    20.5 +(*  Title:      HOLCF/porder0.thy
    20.6      ID:         $Id$
    20.7 -    Author: 	Franz Regensburger
    20.8 +    Author:     Franz Regensburger
    20.9      Copyright   1993 Technische Universitaet Muenchen
   20.10  
   20.11  Definition of class porder (partial order)
   20.12 @@ -20,24 +20,24 @@
   20.13  
   20.14  arities void :: po
   20.15  
   20.16 -consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
   20.17 +consts  "<<"    ::      "['a,'a::po] => bool"   (infixl 55)
   20.18  
   20.19  rules
   20.20  
   20.21  (* class axioms: justification is theory Void *)
   20.22  
   20.23 -refl_less	"x << x"	
   20.24 -				(* witness refl_less_void    *)
   20.25 +refl_less       "x << x"        
   20.26 +                                (* witness refl_less_void    *)
   20.27  
   20.28 -antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
   20.29 -				(* witness antisym_less_void *)
   20.30 +antisym_less    "[|x<<y ; y<<x |] ==> x = y"    
   20.31 +                                (* witness antisym_less_void *)
   20.32  
   20.33 -trans_less	"[|x<<y ; y<<z |] ==> x<<z"
   20.34 -				(* witness trans_less_void   *)
   20.35 +trans_less      "[|x<<y ; y<<z |] ==> x<<z"
   20.36 +                                (* witness trans_less_void   *)
   20.37  
   20.38  (* instance of << for the prototype void *)
   20.39  
   20.40 -inst_void_po	"((op <<)::[void,void]=>bool) = less_void"
   20.41 +inst_void_po    "((op <<)::[void,void]=>bool) = less_void"
   20.42  
   20.43  (* start 8bit 1 *)
   20.44  (* end 8bit 1 *)
    21.1 --- a/src/HOLCF/Sprod0.thy	Tue Feb 06 12:27:17 1996 +0100
    21.2 +++ b/src/HOLCF/Sprod0.thy	Tue Feb 06 12:42:31 1996 +0100
    21.3 @@ -1,6 +1,6 @@
    21.4 -(*  Title: 	HOLCF/sprod0.thy
    21.5 +(*  Title:      HOLCF/sprod0.thy
    21.6      ID:         $Id$
    21.7 -    Author: 	Franz Regensburger
    21.8 +    Author:     Franz Regensburger
    21.9      Copyright   1993  Technische Universitaet Muenchen
   21.10  
   21.11  Strict product
   21.12 @@ -12,43 +12,43 @@
   21.13  
   21.14  types "**" 2        (infixr 20)
   21.15  
   21.16 -arities "**" :: (pcpo,pcpo)term	
   21.17 +arities "**" :: (pcpo,pcpo)term 
   21.18  
   21.19  consts
   21.20 -  Sprod		:: "('a => 'b => bool)set"
   21.21 -  Spair_Rep	:: "['a,'b] => ['a,'b] => bool"
   21.22 -  Rep_Sprod	:: "('a ** 'b) => ('a => 'b => bool)"
   21.23 -  Abs_Sprod	:: "('a => 'b => bool) => ('a ** 'b)"
   21.24 -  Ispair	:: "['a,'b] => ('a ** 'b)"
   21.25 -  Isfst		:: "('a ** 'b) => 'a"
   21.26 -  Issnd		:: "('a ** 'b) => 'b"  
   21.27 +  Sprod         :: "('a => 'b => bool)set"
   21.28 +  Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
   21.29 +  Rep_Sprod     :: "('a ** 'b) => ('a => 'b => bool)"
   21.30 +  Abs_Sprod     :: "('a => 'b => bool) => ('a ** 'b)"
   21.31 +  Ispair        :: "['a,'b] => ('a ** 'b)"
   21.32 +  Isfst         :: "('a ** 'b) => 'a"
   21.33 +  Issnd         :: "('a ** 'b) => 'b"  
   21.34  
   21.35  defs
   21.36 -  Spair_Rep_def		"Spair_Rep == (%a b. %x y.
   21.37 -				(~a=UU & ~b=UU --> x=a  & y=b ))"
   21.38 +  Spair_Rep_def         "Spair_Rep == (%a b. %x y.
   21.39 +                                (~a=UU & ~b=UU --> x=a  & y=b ))"
   21.40  
   21.41 -  Sprod_def		"Sprod == {f. ? a b. f = Spair_Rep a b}"
   21.42 +  Sprod_def             "Sprod == {f. ? a b. f = Spair_Rep a b}"
   21.43  
   21.44  rules
   21.45    (*faking a type definition... *)
   21.46    (* "**" is isomorphic to Sprod *)
   21.47  
   21.48 -  Rep_Sprod		"Rep_Sprod(p):Sprod"		
   21.49 -  Rep_Sprod_inverse	"Abs_Sprod(Rep_Sprod(p)) = p"	
   21.50 -  Abs_Sprod_inverse	"f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
   21.51 +  Rep_Sprod             "Rep_Sprod(p):Sprod"            
   21.52 +  Rep_Sprod_inverse     "Abs_Sprod(Rep_Sprod(p)) = p"   
   21.53 +  Abs_Sprod_inverse     "f:Sprod ==> Rep_Sprod(Abs_Sprod(f)) = f"
   21.54  
   21.55  defs
   21.56     (*defining the abstract constants*)
   21.57  
   21.58 -  Ispair_def	"Ispair a b == Abs_Sprod(Spair_Rep a b)"
   21.59 +  Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
   21.60  
   21.61 -  Isfst_def	"Isfst(p) == @z.
   21.62 -					(p=Ispair UU UU --> z=UU)
   21.63 -		&(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
   21.64 +  Isfst_def     "Isfst(p) == @z.
   21.65 +                                        (p=Ispair UU UU --> z=UU)
   21.66 +                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
   21.67  
   21.68 -  Issnd_def	"Issnd(p) == @z.
   21.69 -					(p=Ispair UU UU  --> z=UU)
   21.70 -		&(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
   21.71 +  Issnd_def     "Issnd(p) == @z.
   21.72 +                                        (p=Ispair UU UU  --> z=UU)
   21.73 +                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
   21.74  
   21.75  (* start 8bit 1 *)
   21.76  (* end 8bit 1 *)
    22.1 --- a/src/HOLCF/Sprod1.thy	Tue Feb 06 12:27:17 1996 +0100
    22.2 +++ b/src/HOLCF/Sprod1.thy	Tue Feb 06 12:42:31 1996 +0100
    22.3 @@ -1,6 +1,6 @@
    22.4 -(*  Title: 	HOLCF/sprod1.thy
    22.5 +(*  Title:      HOLCF/sprod1.thy
    22.6      ID:         $Id$
    22.7 -    Author: 	Franz Regensburger
    22.8 +    Author:     Franz Regensburger
    22.9      Copyright   1993  Technische Universitaet Muenchen
   22.10  
   22.11  Partial ordering for the strict product
   22.12 @@ -9,12 +9,12 @@
   22.13  Sprod1 = Sprod0 +
   22.14  
   22.15  consts
   22.16 -  less_sprod	:: "[('a ** 'b),('a ** 'b)] => bool"	
   22.17 +  less_sprod    :: "[('a ** 'b),('a ** 'b)] => bool"    
   22.18  
   22.19  defs
   22.20    less_sprod_def "less_sprod p1 p2 == 
   22.21 -	if p1 = Ispair UU UU
   22.22 -		then True
   22.23 -		else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   22.24 +        if p1 = Ispair UU UU
   22.25 +                then True
   22.26 +                else Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   22.27  
   22.28  end
    23.1 --- a/src/HOLCF/Sprod2.thy	Tue Feb 06 12:27:17 1996 +0100
    23.2 +++ b/src/HOLCF/Sprod2.thy	Tue Feb 06 12:42:31 1996 +0100
    23.3 @@ -1,6 +1,6 @@
    23.4 -(*  Title: 	HOLCF/sprod2.thy
    23.5 +(*  Title:      HOLCF/sprod2.thy
    23.6      ID:         $Id$
    23.7 -    Author: 	Franz Regensburger
    23.8 +    Author:     Franz Regensburger
    23.9      Copyright   1993 Technische Universitaet Muenchen
   23.10  
   23.11  Class Instance **::(pcpo,pcpo)po
   23.12 @@ -16,7 +16,7 @@
   23.13  
   23.14  (* instance of << for type ['a ** 'b]  *)
   23.15  
   23.16 -inst_sprod_po	"((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
   23.17 +inst_sprod_po   "((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
   23.18  
   23.19  end
   23.20  
    24.1 --- a/src/HOLCF/Sprod3.thy	Tue Feb 06 12:27:17 1996 +0100
    24.2 +++ b/src/HOLCF/Sprod3.thy	Tue Feb 06 12:42:31 1996 +0100
    24.3 @@ -1,6 +1,6 @@
    24.4 -(*  Title: 	HOLCF/sprod3.thy
    24.5 +(*  Title:      HOLCF/sprod3.thy
    24.6      ID:         $Id$
    24.7 -    Author: 	Franz Regensburger
    24.8 +    Author:     Franz Regensburger
    24.9      Copyright   1993 Technische Universitaet Muenchen
   24.10  
   24.11  Class instance of  ** for class pcpo
   24.12 @@ -8,30 +8,30 @@
   24.13  
   24.14  Sprod3 = Sprod2 +
   24.15  
   24.16 -arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
   24.17 +arities "**" :: (pcpo,pcpo)pcpo                 (* Witness sprod2.ML *)
   24.18  
   24.19  consts  
   24.20 -	spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
   24.21 -	sfst         :: "('a**'b)->'a"
   24.22 -	ssnd         :: "('a**'b)->'b"
   24.23 -	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
   24.24 +        spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
   24.25 +        sfst         :: "('a**'b)->'a"
   24.26 +        ssnd         :: "('a**'b)->'b"
   24.27 +        ssplit       :: "('a->'b->'c)->('a**'b)->'c"
   24.28  
   24.29  syntax  
   24.30 -	"@stuple"    :: "['a, args] => 'a ** 'b"	("(1'(|_,/ _|'))")
   24.31 +        "@stuple"    :: "['a, args] => 'a ** 'b"        ("(1'(|_,/ _|'))")
   24.32  
   24.33  translations
   24.34 -	"(|x, y, z|)"   == "(|x, (|y, z|)|)"
   24.35 -	"(|x, y|)"      == "spair`x`y"
   24.36 +        "(|x, y, z|)"   == "(|x, (|y, z|)|)"
   24.37 +        "(|x, y|)"      == "spair`x`y"
   24.38  
   24.39  rules 
   24.40  
   24.41 -inst_sprod_pcpo	"(UU::'a**'b) = Ispair UU UU"
   24.42 +inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU"
   24.43  
   24.44  defs
   24.45 -spair_def	"spair  == (LAM x y.Ispair x y)"
   24.46 -sfst_def	"sfst   == (LAM p.Isfst p)"
   24.47 -ssnd_def	"ssnd   == (LAM p.Issnd p)"	
   24.48 -ssplit_def	"ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
   24.49 +spair_def       "spair  == (LAM x y.Ispair x y)"
   24.50 +sfst_def        "sfst   == (LAM p.Isfst p)"
   24.51 +ssnd_def        "ssnd   == (LAM p.Issnd p)"     
   24.52 +ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
   24.53  
   24.54  (* start 8bit 1 *)
   24.55  (* end 8bit 1 *)
    25.1 --- a/src/HOLCF/Ssum0.thy	Tue Feb 06 12:27:17 1996 +0100
    25.2 +++ b/src/HOLCF/Ssum0.thy	Tue Feb 06 12:42:31 1996 +0100
    25.3 @@ -1,6 +1,6 @@
    25.4 -(*  Title: 	HOLCF/ssum0.thy
    25.5 +(*  Title:      HOLCF/ssum0.thy
    25.6      ID:         $Id$
    25.7 -    Author: 	Franz Regensburger
    25.8 +    Author:     Franz Regensburger
    25.9      Copyright   1993  Technische Universitaet Muenchen
   25.10  
   25.11  Strict sum
   25.12 @@ -12,44 +12,44 @@
   25.13  
   25.14  types "++" 2        (infixr 10)
   25.15  
   25.16 -arities "++" :: (pcpo,pcpo)term	
   25.17 +arities "++" :: (pcpo,pcpo)term 
   25.18  
   25.19  consts
   25.20 -  Ssum		:: "(['a,'b,bool]=>bool)set"
   25.21 -  Sinl_Rep	:: "['a,'a,'b,bool]=>bool"
   25.22 -  Sinr_Rep	:: "['b,'a,'b,bool]=>bool"
   25.23 -  Rep_Ssum	:: "('a ++ 'b) => (['a,'b,bool]=>bool)"
   25.24 -  Abs_Ssum	:: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
   25.25 -  Isinl		:: "'a => ('a ++ 'b)"
   25.26 -  Isinr		:: "'b => ('a ++ 'b)"
   25.27 -  Iwhen		:: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
   25.28 +  Ssum          :: "(['a,'b,bool]=>bool)set"
   25.29 +  Sinl_Rep      :: "['a,'a,'b,bool]=>bool"
   25.30 +  Sinr_Rep      :: "['b,'a,'b,bool]=>bool"
   25.31 +  Rep_Ssum      :: "('a ++ 'b) => (['a,'b,bool]=>bool)"
   25.32 +  Abs_Ssum      :: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
   25.33 +  Isinl         :: "'a => ('a ++ 'b)"
   25.34 +  Isinr         :: "'b => ('a ++ 'b)"
   25.35 +  Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
   25.36  
   25.37  defs
   25.38  
   25.39 -  Sinl_Rep_def		"Sinl_Rep == (%a.%x y p.
   25.40 -				(a~=UU --> x=a  & p))"
   25.41 +  Sinl_Rep_def          "Sinl_Rep == (%a.%x y p.
   25.42 +                                (a~=UU --> x=a  & p))"
   25.43  
   25.44 -  Sinr_Rep_def		"Sinr_Rep == (%b.%x y p.
   25.45 -				(b~=UU --> y=b  & ~p))"
   25.46 +  Sinr_Rep_def          "Sinr_Rep == (%b.%x y p.
   25.47 +                                (b~=UU --> y=b  & ~p))"
   25.48  
   25.49 -  Ssum_def		"Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
   25.50 +  Ssum_def              "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
   25.51  
   25.52  rules
   25.53    (*faking a type definition... *)
   25.54    (* "++" is isomorphic to Ssum *)
   25.55  
   25.56 -  Rep_Ssum		"Rep_Ssum(p):Ssum"		
   25.57 -  Rep_Ssum_inverse	"Abs_Ssum(Rep_Ssum(p)) = p"	
   25.58 -  Abs_Ssum_inverse	"f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
   25.59 +  Rep_Ssum              "Rep_Ssum(p):Ssum"              
   25.60 +  Rep_Ssum_inverse      "Abs_Ssum(Rep_Ssum(p)) = p"     
   25.61 +  Abs_Ssum_inverse      "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
   25.62  
   25.63  defs   (*defining the abstract constants*)
   25.64 -  Isinl_def	"Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
   25.65 -  Isinr_def	"Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
   25.66 +  Isinl_def     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
   25.67 +  Isinr_def     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
   25.68  
   25.69 -  Iwhen_def	"Iwhen(f)(g)(s) == @z.
   25.70 -				    (s=Isinl(UU) --> z=UU)
   25.71 -			&(!a. a~=UU & s=Isinl(a) --> z=f`a)  
   25.72 -			&(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
   25.73 +  Iwhen_def     "Iwhen(f)(g)(s) == @z.
   25.74 +                                    (s=Isinl(UU) --> z=UU)
   25.75 +                        &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
   25.76 +                        &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
   25.77  
   25.78  (* start 8bit 1 *)
   25.79  (* end 8bit 1 *)
    26.1 --- a/src/HOLCF/Ssum1.thy	Tue Feb 06 12:27:17 1996 +0100
    26.2 +++ b/src/HOLCF/Ssum1.thy	Tue Feb 06 12:42:31 1996 +0100
    26.3 @@ -1,6 +1,6 @@
    26.4 -(*  Title: 	HOLCF/ssum1.thy
    26.5 +(*  Title:      HOLCF/ssum1.thy
    26.6      ID:         $Id$
    26.7 -    Author: 	Franz Regensburger
    26.8 +    Author:     Franz Regensburger
    26.9      Copyright   1993  Technische Universitaet Muenchen
   26.10  
   26.11  Partial ordering for the strict sum ++
   26.12 @@ -10,15 +10,15 @@
   26.13  
   26.14  consts
   26.15  
   26.16 -  less_ssum	:: "[('a ++ 'b),('a ++ 'b)] => bool"	
   26.17 +  less_ssum     :: "[('a ++ 'b),('a ++ 'b)] => bool"    
   26.18  
   26.19  rules
   26.20  
   26.21    less_ssum_def "less_ssum s1 s2 == (@z.
   26.22 -	 (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
   26.23 -	&(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
   26.24 -	&(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
   26.25 -	&(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
   26.26 +         (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x))
   26.27 +        &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y))
   26.28 +        &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU))
   26.29 +        &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))"
   26.30  
   26.31  end
   26.32  
    27.1 --- a/src/HOLCF/Ssum2.thy	Tue Feb 06 12:27:17 1996 +0100
    27.2 +++ b/src/HOLCF/Ssum2.thy	Tue Feb 06 12:42:31 1996 +0100
    27.3 @@ -1,6 +1,6 @@
    27.4 -(*  Title: 	HOLCF/ssum2.thy
    27.5 +(*  Title:      HOLCF/ssum2.thy
    27.6      ID:         $Id$
    27.7 -    Author: 	Franz Regensburger
    27.8 +    Author:     Franz Regensburger
    27.9      Copyright   1993 Technische Universitaet Muenchen
   27.10  
   27.11  Class Instance ++::(pcpo,pcpo)po
   27.12 @@ -15,7 +15,7 @@
   27.13  
   27.14  (* instance of << for type ['a ++ 'b]  *)
   27.15  
   27.16 -inst_ssum_po	"((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
   27.17 +inst_ssum_po    "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
   27.18  
   27.19  end
   27.20  
    28.1 --- a/src/HOLCF/Ssum3.thy	Tue Feb 06 12:27:17 1996 +0100
    28.2 +++ b/src/HOLCF/Ssum3.thy	Tue Feb 06 12:42:31 1996 +0100
    28.3 @@ -1,6 +1,6 @@
    28.4 -(*  Title: 	HOLCF/ssum3.thy
    28.5 +(*  Title:      HOLCF/ssum3.thy
    28.6      ID:         $Id$
    28.7 -    Author: 	Franz Regensburger
    28.8 +    Author:     Franz Regensburger
    28.9      Copyright   1993 Technische Universitaet Muenchen
   28.10  
   28.11  Class instance of  ++ for class pcpo
   28.12 @@ -8,23 +8,23 @@
   28.13  
   28.14  Ssum3 = Ssum2 +
   28.15  
   28.16 -arities "++" :: (pcpo,pcpo)pcpo			(* Witness ssum2.ML *)
   28.17 +arities "++" :: (pcpo,pcpo)pcpo                 (* Witness ssum2.ML *)
   28.18  
   28.19  consts  
   28.20 -	sinl	:: "'a -> ('a++'b)" 
   28.21 -	sinr	:: "'b -> ('a++'b)" 
   28.22 -	sswhen	:: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
   28.23 +        sinl    :: "'a -> ('a++'b)" 
   28.24 +        sinr    :: "'b -> ('a++'b)" 
   28.25 +        sswhen  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"
   28.26  
   28.27  rules 
   28.28  
   28.29 -inst_ssum_pcpo	"(UU::'a++'b) = Isinl(UU)"
   28.30 +inst_ssum_pcpo  "(UU::'a++'b) = Isinl(UU)"
   28.31  
   28.32  
   28.33  defs
   28.34  
   28.35 -sinl_def	"sinl   == (LAM x.Isinl(x))"
   28.36 -sinr_def	"sinr   == (LAM x.Isinr(x))"
   28.37 -sswhen_def	"sswhen   == (LAM f g s.Iwhen(f)(g)(s))"
   28.38 +sinl_def        "sinl   == (LAM x.Isinl(x))"
   28.39 +sinr_def        "sinr   == (LAM x.Isinr(x))"
   28.40 +sswhen_def      "sswhen   == (LAM f g s.Iwhen(f)(g)(s))"
   28.41  
   28.42  translations
   28.43  "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
    29.1 --- a/src/HOLCF/Tr1.thy	Tue Feb 06 12:27:17 1996 +0100
    29.2 +++ b/src/HOLCF/Tr1.thy	Tue Feb 06 12:42:31 1996 +0100
    29.3 @@ -1,6 +1,6 @@
    29.4 -(*  Title: 	HOLCF/tr1.thy
    29.5 +(*  Title:      HOLCF/tr1.thy
    29.6      ID:         $Id$
    29.7 -    Author: 	Franz Regensburger
    29.8 +    Author:     Franz Regensburger
    29.9      Copyright   1993 Technische Universitaet Muenchen
   29.10  
   29.11  Introduce the domain of truth values tr = one ++ one
   29.12 @@ -23,24 +23,24 @@
   29.13  arities tr :: pcpo
   29.14  
   29.15  consts
   29.16 -	abs_tr		:: "one ++ one -> tr"
   29.17 -	rep_tr		:: "tr -> one ++ one"
   29.18 -	TT 		:: "tr"
   29.19 -	FF		:: "tr"
   29.20 -	tr_when 	:: "'c -> 'c -> tr -> 'c"
   29.21 +        abs_tr          :: "one ++ one -> tr"
   29.22 +        rep_tr          :: "tr -> one ++ one"
   29.23 +        TT              :: "tr"
   29.24 +        FF              :: "tr"
   29.25 +        tr_when         :: "'c -> 'c -> tr -> 'c"
   29.26  
   29.27  rules
   29.28  
   29.29 -  abs_tr_iso	"abs_tr`(rep_tr`u) = u"
   29.30 -  rep_tr_iso	"rep_tr`(abs_tr`x) = x"
   29.31 +  abs_tr_iso    "abs_tr`(rep_tr`u) = u"
   29.32 +  rep_tr_iso    "rep_tr`(abs_tr`x) = x"
   29.33  
   29.34  defs
   29.35  
   29.36 -  TT_def	"TT == abs_tr`(sinl`one)"
   29.37 -  FF_def	"FF == abs_tr`(sinr`one)"
   29.38 +  TT_def        "TT == abs_tr`(sinl`one)"
   29.39 +  FF_def        "FF == abs_tr`(sinr`one)"
   29.40  
   29.41    tr_when_def "tr_when == 
   29.42 -	(LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
   29.43 +        (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))"
   29.44  
   29.45  (* start 8bit 1 *)
   29.46  (* end 8bit 1 *)
    30.1 --- a/src/HOLCF/Tr2.thy	Tue Feb 06 12:27:17 1996 +0100
    30.2 +++ b/src/HOLCF/Tr2.thy	Tue Feb 06 12:42:31 1996 +0100
    30.3 @@ -1,6 +1,6 @@
    30.4 -(*  Title: 	HOLCF/tr2.thy
    30.5 +(*  Title:      HOLCF/tr2.thy
    30.6      ID:         $Id$
    30.7 -    Author: 	Franz Regensburger
    30.8 +    Author:     Franz Regensburger
    30.9      Copyright   1993 Technische Universitaet Muenchen
   30.10  
   30.11  Introduce infix if_then_else_fi and boolean connectives andalso, orelse
   30.12 @@ -9,15 +9,15 @@
   30.13  Tr2 = Tr1 +
   30.14  
   30.15  consts
   30.16 -	Icifte		:: "tr -> 'c -> 'c -> 'c"
   30.17 -	trand		:: "tr -> tr -> tr"
   30.18 -	tror		:: "tr -> tr -> tr"
   30.19 -        neg		:: "tr -> tr"
   30.20 +        Icifte          :: "tr -> 'c -> 'c -> 'c"
   30.21 +        trand           :: "tr -> tr -> tr"
   30.22 +        tror            :: "tr -> tr -> tr"
   30.23 +        neg             :: "tr -> tr"
   30.24  
   30.25 -syntax 	"@cifte"	:: "tr=>'c=>'c=>'c"
   30.26 +syntax  "@cifte"        :: "tr=>'c=>'c=>'c"
   30.27                               ("(3If _/ (then _/ else _) fi)" 60)
   30.28 -	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
   30.29 -	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
   30.30 +        "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
   30.31 +        "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
   30.32   
   30.33  translations "x andalso y" == "trand`x`y"
   30.34               "x orelse y"  == "tror`x`y"
    31.1 --- a/src/HOLCF/Void.thy	Tue Feb 06 12:27:17 1996 +0100
    31.2 +++ b/src/HOLCF/Void.thy	Tue Feb 06 12:42:31 1996 +0100
    31.3 @@ -1,6 +1,6 @@
    31.4 -(*  Title: 	HOLCF/void.thy
    31.5 +(*  Title:      HOLCF/void.thy
    31.6      ID:         $Id$
    31.7 -    Author: 	Franz Regensburger
    31.8 +    Author:     Franz Regensburger
    31.9      Copyright   1993  Technische Universitaet Muenchen
   31.10  
   31.11  Definition of type void with partial order. Void is the prototype for
   31.12 @@ -16,23 +16,23 @@
   31.13  arities void :: term
   31.14  
   31.15  consts
   31.16 -  Void		:: "bool set"
   31.17 -  UU_void_Rep	:: "bool"	
   31.18 -  Rep_Void	:: "void => bool"
   31.19 -  Abs_Void	:: "bool => void"
   31.20 -  UU_void	:: "void"
   31.21 -  less_void	:: "[void,void] => bool"	
   31.22 +  Void          :: "bool set"
   31.23 +  UU_void_Rep   :: "bool"       
   31.24 +  Rep_Void      :: "void => bool"
   31.25 +  Abs_Void      :: "bool => void"
   31.26 +  UU_void       :: "void"
   31.27 +  less_void     :: "[void,void] => bool"        
   31.28  
   31.29  defs
   31.30  
   31.31    (* The unique element in Void is False:bool *)
   31.32  
   31.33 -  UU_void_Rep_def	"UU_void_Rep == False"
   31.34 -  Void_def		"Void == {x. x = UU_void_Rep}"
   31.35 +  UU_void_Rep_def       "UU_void_Rep == False"
   31.36 +  Void_def              "Void == {x. x = UU_void_Rep}"
   31.37  
   31.38     (*defining the abstract constants*)
   31.39  
   31.40 -  UU_void_def	"UU_void == Abs_Void(UU_void_Rep)"  
   31.41 +  UU_void_def   "UU_void == Abs_Void(UU_void_Rep)"  
   31.42    less_void_def "less_void x y == (Rep_Void x = Rep_Void y)"  
   31.43  
   31.44  rules
   31.45 @@ -40,9 +40,9 @@
   31.46    (*faking a type definition... *)
   31.47    (* void is isomorphic to Void *)
   31.48  
   31.49 -  Rep_Void		"Rep_Void(x):Void"		
   31.50 -  Rep_Void_inverse	"Abs_Void(Rep_Void(x)) = x"	
   31.51 -  Abs_Void_inverse	"y:Void ==> Rep_Void(Abs_Void(y)) = y"
   31.52 +  Rep_Void              "Rep_Void(x):Void"              
   31.53 +  Rep_Void_inverse      "Abs_Void(Rep_Void(x)) = x"     
   31.54 +  Abs_Void_inverse      "y:Void ==> Rep_Void(Abs_Void(y)) = y"
   31.55  
   31.56  end
   31.57  
    32.1 --- a/src/HOLCF/ccc1.thy	Tue Feb 06 12:27:17 1996 +0100
    32.2 +++ b/src/HOLCF/ccc1.thy	Tue Feb 06 12:42:31 1996 +0100
    32.3 @@ -1,6 +1,6 @@
    32.4 -(*  Title: 	HOLCF/ccc1.thy
    32.5 +(*  Title:      HOLCF/ccc1.thy
    32.6      ID:         $Id$
    32.7 -    Author: 	Franz Regensburger
    32.8 +    Author:     Franz Regensburger
    32.9      Copyright   1993 Technische Universitaet Muenchen
   32.10  
   32.11  Merge Theories Cprof, Sprod, Ssum, Lift, Fix and
   32.12 @@ -10,17 +10,17 @@
   32.13  ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
   32.14  
   32.15  consts
   32.16 -	ID 	:: "'a -> 'a"
   32.17 -	cfcomp	:: "('b->'c)->('a->'b)->'a->'c"
   32.18 +        ID      :: "'a -> 'a"
   32.19 +        cfcomp  :: "('b->'c)->('a->'b)->'a->'c"
   32.20  
   32.21 -syntax	"@oo"	:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
   32.22 +syntax  "@oo"   :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
   32.23       
   32.24 -translations 	"f1 oo f2" == "cfcomp`f1`f2"
   32.25 +translations    "f1 oo f2" == "cfcomp`f1`f2"
   32.26  
   32.27  defs
   32.28  
   32.29 -  ID_def	"ID ==(LAM x.x)"
   32.30 -  oo_def	"cfcomp == (LAM f g x.f`(g`x))" 
   32.31 +  ID_def        "ID ==(LAM x.x)"
   32.32 +  oo_def        "cfcomp == (LAM f g x.f`(g`x))" 
   32.33  
   32.34  end
   32.35  
    33.1 --- a/src/HOLCF/ex/Fix2.thy	Tue Feb 06 12:27:17 1996 +0100
    33.2 +++ b/src/HOLCF/ex/Fix2.thy	Tue Feb 06 12:42:31 1996 +0100
    33.3 @@ -1,7 +1,7 @@
    33.4 -(*  Title:	HOLCF/ex/Fix2.thy
    33.5 +(*  Title:      HOLCF/ex/Fix2.thy
    33.6      ID:         $Id$
    33.7 -    Author: 	Franz Regensburger
    33.8 -    Copyright	1995 Technische Universitaet Muenchen
    33.9 +    Author:     Franz Regensburger
   33.10 +    Copyright   1995 Technische Universitaet Muenchen
   33.11  
   33.12   Show that fix is the unique least fixed-point operator. 
   33.13   From axioms gix1_def,gix2_def it follows that fix = gix
    34.1 --- a/src/HOLCF/ex/Hoare.thy	Tue Feb 06 12:27:17 1996 +0100
    34.2 +++ b/src/HOLCF/ex/Hoare.thy	Tue Feb 06 12:42:31 1996 +0100
    34.3 @@ -1,7 +1,7 @@
    34.4 -(*  Title:	HOLCF/ex/hoare.thy
    34.5 +(*  Title:      HOLCF/ex/hoare.thy
    34.6      ID:         $Id$
    34.7 -    Author: 	Franz Regensburger
    34.8 -    Copyright	1993 Technische Universitaet Muenchen
    34.9 +    Author:     Franz Regensburger
   34.10 +    Copyright   1993 Technische Universitaet Muenchen
   34.11  
   34.12  Theory for an example by C.A.R. Hoare 
   34.13  
   34.14 @@ -24,11 +24,11 @@
   34.15  Hoare = Tr2 +
   34.16  
   34.17  consts
   34.18 -	b1:: "'a -> tr"
   34.19 -	b2:: "'a -> tr"
   34.20 -	 g:: "'a -> 'a"
   34.21 -	p :: "'a -> 'a"
   34.22 -	q :: "'a -> 'a"
   34.23 +        b1:: "'a -> tr"
   34.24 +        b2:: "'a -> tr"
   34.25 +         g:: "'a -> 'a"
   34.26 +        p :: "'a -> 'a"
   34.27 +        q :: "'a -> 'a"
   34.28  
   34.29  defs
   34.30  
    35.1 --- a/src/HOLCF/ex/Loop.thy	Tue Feb 06 12:27:17 1996 +0100
    35.2 +++ b/src/HOLCF/ex/Loop.thy	Tue Feb 06 12:42:31 1996 +0100
    35.3 @@ -1,7 +1,7 @@
    35.4 -(*  Title:	HOLCF/ex/Loop.thy
    35.5 +(*  Title:      HOLCF/ex/Loop.thy
    35.6      ID:         $Id$
    35.7 -    Author: 	Franz Regensburger
    35.8 -    Copyright	1993 Technische Universitaet Muenchen
    35.9 +    Author:     Franz Regensburger
   35.10 +    Copyright   1993 Technische Universitaet Muenchen
   35.11  
   35.12  Theory for a loop primitive like while
   35.13  *)
   35.14 @@ -10,13 +10,13 @@
   35.15  
   35.16  consts
   35.17  
   35.18 -	step  :: "('a -> tr)->('a -> 'a)->'a->'a"
   35.19 -	while :: "('a -> tr)->('a -> 'a)->'a->'a"
   35.20 +        step  :: "('a -> tr)->('a -> 'a)->'a->'a"
   35.21 +        while :: "('a -> tr)->('a -> 'a)->'a->'a"
   35.22  
   35.23  defs
   35.24  
   35.25 -  step_def	"step == (LAM b g x. If b`x then g`x else x fi)"
   35.26 -  while_def	"while == (LAM b g. fix`(LAM f x.
   35.27 +  step_def      "step == (LAM b g x. If b`x then g`x else x fi)"
   35.28 +  while_def     "while == (LAM b g. fix`(LAM f x.
   35.29                     If b`x then f`(g`x) else x fi))"
   35.30  
   35.31  end
    36.1 --- a/src/HOLCF/explicit_domains/Coind.thy	Tue Feb 06 12:27:17 1996 +0100
    36.2 +++ b/src/HOLCF/explicit_domains/Coind.thy	Tue Feb 06 12:42:31 1996 +0100
    36.3 @@ -1,6 +1,6 @@
    36.4 -(*  Title: 	HOLCF/Coind.thy
    36.5 +(*  Title:      HOLCF/Coind.thy
    36.6      ID:         $Id$
    36.7 -    Author: 	Franz Regensburger
    36.8 +    Author:     Franz Regensburger
    36.9      Copyright   1993 Technische Universitaet Muenchen
   36.10  
   36.11  Example for co-induction on streams
   36.12 @@ -11,23 +11,23 @@
   36.13  
   36.14  consts
   36.15  
   36.16 -	nats		:: "dnat stream"
   36.17 -	from		:: "dnat -> dnat stream"
   36.18 +        nats            :: "dnat stream"
   36.19 +        from            :: "dnat -> dnat stream"
   36.20  
   36.21  defs
   36.22 -	nats_def	"nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
   36.23 +        nats_def        "nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
   36.24  
   36.25 -	from_def	"from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
   36.26 +        from_def        "from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
   36.27  
   36.28  end
   36.29  
   36.30  (*
   36.31 -		smap`f`UU = UU
   36.32 +                smap`f`UU = UU
   36.33        x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs)
   36.34  
   36.35 -		nats = scons`dzero`(smap`dsucc`nats)
   36.36 +                nats = scons`dzero`(smap`dsucc`nats)
   36.37  
   36.38 -		from`n = scons`n`(from`(dsucc`n))
   36.39 +                from`n = scons`n`(from`(dsucc`n))
   36.40  *)
   36.41  
   36.42  
    37.1 --- a/src/HOLCF/explicit_domains/Dagstuhl.thy	Tue Feb 06 12:27:17 1996 +0100
    37.2 +++ b/src/HOLCF/explicit_domains/Dagstuhl.thy	Tue Feb 06 12:42:31 1996 +0100
    37.3 @@ -4,7 +4,7 @@
    37.4  Dagstuhl  =  Stream2 +
    37.5  
    37.6  consts
    37.7 -	y  :: "'a"
    37.8 +        y  :: "'a"
    37.9         YS  :: "'a stream"
   37.10         YYS :: "'a stream"
   37.11  
    38.1 --- a/src/HOLCF/explicit_domains/Dlist.thy	Tue Feb 06 12:27:17 1996 +0100
    38.2 +++ b/src/HOLCF/explicit_domains/Dlist.thy	Tue Feb 06 12:42:31 1996 +0100
    38.3 @@ -1,6 +1,6 @@
    38.4 -(*  Title: 	HOLCF/Dlist.thy
    38.5 +(*  Title:      HOLCF/Dlist.thy
    38.6  
    38.7 -    Author: 	Franz Regensburger
    38.8 +    Author:     Franz Regensburger
    38.9      ID:         $ $
   38.10      Copyright   1994 Technische Universitaet Muenchen
   38.11  
   38.12 @@ -34,24 +34,24 @@
   38.13  (* ----------------------------------------------------------------------- *)
   38.14  (* essential constants                                                     *)
   38.15  
   38.16 -dlist_rep	:: "('a dlist) -> (one ++ 'a ** 'a dlist)"
   38.17 -dlist_abs	:: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
   38.18 +dlist_rep       :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
   38.19 +dlist_abs       :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
   38.20  
   38.21  (* ----------------------------------------------------------------------- *)
   38.22  (* abstract constants and auxiliary constants                              *)
   38.23  
   38.24 -dlist_copy	:: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
   38.25 +dlist_copy      :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
   38.26  
   38.27  dnil            :: "'a dlist"
   38.28 -dcons		:: "'a -> 'a dlist -> 'a dlist"
   38.29 -dlist_when	:: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
   38.30 -is_dnil    	:: "'a dlist -> tr"
   38.31 -is_dcons	:: "'a dlist -> tr"
   38.32 -dhd		:: "'a dlist -> 'a"
   38.33 -dtl		:: "'a dlist -> 'a dlist"
   38.34 -dlist_take	:: "nat => 'a dlist -> 'a dlist"
   38.35 -dlist_finite	:: "'a dlist => bool"
   38.36 -dlist_bisim	:: "('a dlist => 'a dlist => bool) => bool"
   38.37 +dcons           :: "'a -> 'a dlist -> 'a dlist"
   38.38 +dlist_when      :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
   38.39 +is_dnil         :: "'a dlist -> tr"
   38.40 +is_dcons        :: "'a dlist -> tr"
   38.41 +dhd             :: "'a dlist -> 'a"
   38.42 +dtl             :: "'a dlist -> 'a dlist"
   38.43 +dlist_take      :: "nat => 'a dlist -> 'a dlist"
   38.44 +dlist_finite    :: "'a dlist => bool"
   38.45 +dlist_bisim     :: "('a dlist => 'a dlist => bool) => bool"
   38.46  
   38.47  rules
   38.48  
   38.49 @@ -66,12 +66,12 @@
   38.50  (* dlist_abs is an isomorphism with inverse dlist_rep                      *)
   38.51  (* identity is the least endomorphism on 'a dlist                          *)
   38.52  
   38.53 -dlist_abs_iso	"dlist_rep`(dlist_abs`x) = x"
   38.54 -dlist_rep_iso	"dlist_abs`(dlist_rep`x) = x"
   38.55 -dlist_copy_def	"dlist_copy == (LAM f. dlist_abs oo \
   38.56 -\ 		(sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
   38.57 +dlist_abs_iso   "dlist_rep`(dlist_abs`x) = x"
   38.58 +dlist_rep_iso   "dlist_abs`(dlist_rep`x) = x"
   38.59 +dlist_copy_def  "dlist_copy == (LAM f. dlist_abs oo \
   38.60 +\               (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
   38.61  \                                oo dlist_rep)"
   38.62 -dlist_reach	"(fix`dlist_copy)`x=x"
   38.63 +dlist_reach     "(fix`dlist_copy)`x=x"
   38.64  
   38.65  
   38.66  defs
   38.67 @@ -80,8 +80,8 @@
   38.68  (* ----------------------------------------------------------------------- *)
   38.69  (* constructors                                                            *)
   38.70  
   38.71 -dnil_def	"dnil  == dlist_abs`(sinl`one)"
   38.72 -dcons_def	"dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
   38.73 +dnil_def        "dnil  == dlist_abs`(sinl`one)"
   38.74 +dcons_def       "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
   38.75  
   38.76  (* ----------------------------------------------------------------------- *)
   38.77  (* discriminator functional                                                *)
   38.78 @@ -93,10 +93,10 @@
   38.79  (* ----------------------------------------------------------------------- *)
   38.80  (* discriminators and selectors                                            *)
   38.81  
   38.82 -is_dnil_def	"is_dnil  == dlist_when`TT`(LAM x l.FF)"
   38.83 -is_dcons_def	"is_dcons == dlist_when`FF`(LAM x l.TT)"
   38.84 -dhd_def		"dhd == dlist_when`UU`(LAM x l.x)"
   38.85 -dtl_def		"dtl == dlist_when`UU`(LAM x l.l)"
   38.86 +is_dnil_def     "is_dnil  == dlist_when`TT`(LAM x l.FF)"
   38.87 +is_dcons_def    "is_dcons == dlist_when`FF`(LAM x l.TT)"
   38.88 +dhd_def         "dhd == dlist_when`UU`(LAM x l.x)"
   38.89 +dtl_def         "dtl == dlist_when`UU`(LAM x l.l)"
   38.90  
   38.91  (* ----------------------------------------------------------------------- *)
   38.92  (* the taker for dlists                                                   *)
   38.93 @@ -105,7 +105,7 @@
   38.94  
   38.95  (* ----------------------------------------------------------------------- *)
   38.96  
   38.97 -dlist_finite_def	"dlist_finite == (%s.? n.dlist_take n`s=s)"
   38.98 +dlist_finite_def        "dlist_finite == (%s.? n.dlist_take n`s=s)"
   38.99  
  38.100  (* ----------------------------------------------------------------------- *)
  38.101  (* definition of bisimulation is determined by domain equation             *)
  38.102 @@ -113,7 +113,7 @@
  38.103  
  38.104  dlist_bisim_def "dlist_bisim ==
  38.105   ( %R.!l1 l2.
  38.106 - 	R l1 l2 -->
  38.107 +        R l1 l2 -->
  38.108    ((l1=UU & l2=UU) |
  38.109     (l1=dnil & l2=dnil) |
  38.110     (? x l11 l21. x~=UU & l11~=UU & l21~=UU & 
    39.1 --- a/src/HOLCF/explicit_domains/Dnat.thy	Tue Feb 06 12:27:17 1996 +0100
    39.2 +++ b/src/HOLCF/explicit_domains/Dnat.thy	Tue Feb 06 12:42:31 1996 +0100
    39.3 @@ -1,6 +1,6 @@
    39.4 -(*  Title: 	HOLCF/Dnat.thy
    39.5 +(*  Title:      HOLCF/Dnat.thy
    39.6      ID:         $Id$
    39.7 -    Author: 	Franz Regensburger
    39.8 +    Author:     Franz Regensburger
    39.9      Copyright   1993 Technische Universitaet Muenchen
   39.10  
   39.11  Theory for the domain of natural numbers  dnat = one ++ dnat
   39.12 @@ -31,22 +31,22 @@
   39.13  (* ----------------------------------------------------------------------- *)
   39.14  (* essential constants                                                     *)
   39.15  
   39.16 -dnat_rep	:: " dnat -> (one ++ dnat)"
   39.17 -dnat_abs	:: "(one ++ dnat) -> dnat"
   39.18 +dnat_rep        :: " dnat -> (one ++ dnat)"
   39.19 +dnat_abs        :: "(one ++ dnat) -> dnat"
   39.20  
   39.21  (* ----------------------------------------------------------------------- *)
   39.22  (* abstract constants and auxiliary constants                              *)
   39.23  
   39.24 -dnat_copy	:: "(dnat -> dnat) -> dnat -> dnat"
   39.25 +dnat_copy       :: "(dnat -> dnat) -> dnat -> dnat"
   39.26  
   39.27 -dzero		:: "dnat"
   39.28 -dsucc		:: "dnat -> dnat"
   39.29 -dnat_when	:: "'b -> (dnat -> 'b) -> dnat -> 'b"
   39.30 -is_dzero	:: "dnat -> tr"
   39.31 -is_dsucc	:: "dnat -> tr"
   39.32 -dpred		:: "dnat -> dnat"
   39.33 -dnat_take	:: "nat => dnat -> dnat"
   39.34 -dnat_bisim	:: "(dnat => dnat => bool) => bool"
   39.35 +dzero           :: "dnat"
   39.36 +dsucc           :: "dnat -> dnat"
   39.37 +dnat_when       :: "'b -> (dnat -> 'b) -> dnat -> 'b"
   39.38 +is_dzero        :: "dnat -> tr"
   39.39 +is_dsucc        :: "dnat -> tr"
   39.40 +dpred           :: "dnat -> dnat"
   39.41 +dnat_take       :: "nat => dnat -> dnat"
   39.42 +dnat_bisim      :: "(dnat => dnat => bool) => bool"
   39.43  
   39.44  rules
   39.45  
   39.46 @@ -61,11 +61,11 @@
   39.47  (* dnat_abs is an isomorphism with inverse dnat_rep                        *)
   39.48  (* identity is the least endomorphism on dnat                              *)
   39.49  
   39.50 -dnat_abs_iso	"dnat_rep`(dnat_abs`x) = x"
   39.51 -dnat_rep_iso	"dnat_abs`(dnat_rep`x) = x"
   39.52 -dnat_copy_def	"dnat_copy == (LAM f. dnat_abs oo 
   39.53 -		 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
   39.54 -dnat_reach	"(fix`dnat_copy)`x=x"
   39.55 +dnat_abs_iso    "dnat_rep`(dnat_abs`x) = x"
   39.56 +dnat_rep_iso    "dnat_abs`(dnat_rep`x) = x"
   39.57 +dnat_copy_def   "dnat_copy == (LAM f. dnat_abs oo 
   39.58 +                 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
   39.59 +dnat_reach      "(fix`dnat_copy)`x=x"
   39.60  
   39.61  
   39.62  defs
   39.63 @@ -74,21 +74,21 @@
   39.64  (* ----------------------------------------------------------------------- *)
   39.65  (* constructors                                                            *)
   39.66  
   39.67 -dzero_def	"dzero == dnat_abs`(sinl`one)"
   39.68 -dsucc_def	"dsucc == (LAM n. dnat_abs`(sinr`n))"
   39.69 +dzero_def       "dzero == dnat_abs`(sinl`one)"
   39.70 +dsucc_def       "dsucc == (LAM n. dnat_abs`(sinr`n))"
   39.71  
   39.72  (* ----------------------------------------------------------------------- *)
   39.73  (* discriminator functional                                                *)
   39.74  
   39.75 -dnat_when_def	"dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
   39.76 +dnat_when_def   "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
   39.77  
   39.78  
   39.79  (* ----------------------------------------------------------------------- *)
   39.80  (* discriminators and selectors                                            *)
   39.81  
   39.82 -is_dzero_def	"is_dzero == dnat_when`TT`(LAM x.FF)"
   39.83 -is_dsucc_def	"is_dsucc == dnat_when`FF`(LAM x.TT)"
   39.84 -dpred_def	"dpred == dnat_when`UU`(LAM x.x)"
   39.85 +is_dzero_def    "is_dzero == dnat_when`TT`(LAM x.FF)"
   39.86 +is_dsucc_def    "is_dsucc == dnat_when`FF`(LAM x.TT)"
   39.87 +dpred_def       "dpred == dnat_when`UU`(LAM x.x)"
   39.88  
   39.89  
   39.90  (* ----------------------------------------------------------------------- *)
   39.91 @@ -102,9 +102,9 @@
   39.92  
   39.93  dnat_bisim_def "dnat_bisim ==
   39.94  (%R.!s1 s2.
   39.95 - 	R s1 s2 -->
   39.96 +        R s1 s2 -->
   39.97    ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
   39.98    (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
   39.99 -		 s2 = dsucc`s21 & R s11 s21)))"
  39.100 +                 s2 = dsucc`s21 & R s11 s21)))"
  39.101  
  39.102  end
    40.1 --- a/src/HOLCF/explicit_domains/Dnat2.thy	Tue Feb 06 12:27:17 1996 +0100
    40.2 +++ b/src/HOLCF/explicit_domains/Dnat2.thy	Tue Feb 06 12:42:31 1996 +0100
    40.3 @@ -1,6 +1,6 @@
    40.4 -(*  Title: 	HOLCF/Dnat2.thy
    40.5 +(*  Title:      HOLCF/Dnat2.thy
    40.6      ID:         $Id$
    40.7 -    Author: 	Franz Regensburger
    40.8 +    Author:     Franz Regensburger
    40.9      Copyright   1993 Technische Universitaet Muenchen
   40.10  
   40.11  Additional constants for dnat
   40.12 @@ -11,19 +11,19 @@
   40.13  
   40.14  consts
   40.15  
   40.16 -iterator	:: "dnat -> ('a -> 'a) -> 'a -> 'a"
   40.17 +iterator        :: "dnat -> ('a -> 'a) -> 'a -> 'a"
   40.18  
   40.19  
   40.20  defs
   40.21  
   40.22 -iterator_def	"iterator == fix`(LAM h n f x.
   40.23 -			dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
   40.24 +iterator_def    "iterator == fix`(LAM h n f x.
   40.25 +                        dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
   40.26  end
   40.27  
   40.28  (*
   40.29  
   40.30 -		iterator`UU`f`x = UU
   40.31 -		iterator`dzero`f`x = x
   40.32 +                iterator`UU`f`x = UU
   40.33 +                iterator`dzero`f`x = x
   40.34        n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
   40.35  *)
   40.36  
    41.1 --- a/src/HOLCF/explicit_domains/Focus_ex.thy	Tue Feb 06 12:27:17 1996 +0100
    41.2 +++ b/src/HOLCF/explicit_domains/Focus_ex.thy	Tue Feb 06 12:42:31 1996 +0100
    41.3 @@ -1,6 +1,6 @@
    41.4  (*
    41.5      ID:         $Id$
    41.6 -    Author: 	Franz Regensburger
    41.7 +    Author:     Franz Regensburger
    41.8      Copyright   1995 Technische Universitaet Muenchen
    41.9  
   41.10  *)
   41.11 @@ -27,17 +27,17 @@
   41.12  -----------------------------------------------------------------
   41.13  
   41.14  agent f
   41.15 -	input  channel i1:'b i2: ('b,'c) tc
   41.16 -	output channel o1:'c o2: ('b,'c) tc
   41.17 +        input  channel i1:'b i2: ('b,'c) tc
   41.18 +        output channel o1:'c o2: ('b,'c) tc
   41.19  is
   41.20 -	Rf(i1,i2,o1,o2)  (left open in the example)
   41.21 +        Rf(i1,i2,o1,o2)  (left open in the example)
   41.22  end f
   41.23  
   41.24  agent g
   41.25 -	input  channel x:'b 
   41.26 -	output channel y:'c 
   41.27 +        input  channel x:'b 
   41.28 +        output channel y:'c 
   41.29  is network
   41.30 -	<y,z> = f`<x,z>
   41.31 +        <y,z> = f`<x,z>
   41.32  end network
   41.33  end g
   41.34  
   41.35 @@ -51,37 +51,37 @@
   41.36  Specification of agent f ist translated to predicate is_f
   41.37  
   41.38  is_f :: ('b stream * ('b,'c) tc stream -> 
   41.39 -		'c stream * ('b,'c) tc stream) => bool
   41.40 +                'c stream * ('b,'c) tc stream) => bool
   41.41  
   41.42  is_f f  = ! i1 i2 o1 o2. 
   41.43 -	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
   41.44 +        f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
   41.45  
   41.46  Specification of agent g is translated to predicate is_g which uses
   41.47  predicate is_net_g
   41.48  
   41.49  is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
   41.50 -	    'b stream => 'c stream => bool
   41.51 +            'b stream => 'c stream => bool
   41.52  
   41.53  is_net_g f x y = 
   41.54 -	? z. <y,z> = f`<x,z> &
   41.55 -	! oy hz. <oy,hz> = f`<x,hz> --> z << hz 
   41.56 +        ? z. <y,z> = f`<x,z> &
   41.57 +        ! oy hz. <oy,hz> = f`<x,hz> --> z << hz 
   41.58  
   41.59  
   41.60  is_g :: ('b stream -> 'c stream) => bool
   41.61  
   41.62  is_g g  = ? f. is_f f  & (! x y. g`x = y --> is_net_g f x y
   41.63 -	  
   41.64 +          
   41.65  Third step: (show conservativity)
   41.66  -----------
   41.67  
   41.68  Suppose we have a model for the theory TH1 which contains the axiom
   41.69  
   41.70 -	? f. is_f f 
   41.71 +        ? f. is_f f 
   41.72  
   41.73  In this case there is also a model for the theory TH2 that enriches TH1 by
   41.74  axiom
   41.75  
   41.76 -	? g. is_g g 
   41.77 +        ? g. is_g g 
   41.78  
   41.79  The result is proved by showing that there is a definitional extension
   41.80  that extends TH1 by a definition of g.
   41.81 @@ -91,17 +91,17 @@
   41.82  
   41.83  def_g g  = 
   41.84           (? f. is_f f  & 
   41.85 -	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
   41.86 -	
   41.87 +              g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
   41.88 +        
   41.89  Now we prove:
   41.90  
   41.91 -	(?f. is_f f ) --> (? g. is_g g) 
   41.92 +        (?f. is_f f ) --> (? g. is_g g) 
   41.93  
   41.94  using the theorems
   41.95  
   41.96 -loopback_eq)	def_g = is_g			(real work) 
   41.97 +loopback_eq)    def_g = is_g                    (real work) 
   41.98  
   41.99 -L1)		(? f. is_f f ) --> (? g. def_g g)  (trivial)
  41.100 +L1)             (? f. is_f f ) --> (? g. def_g g)  (trivial)
  41.101  
  41.102  *)
  41.103  
  41.104 @@ -116,28 +116,28 @@
  41.105  is_f     ::
  41.106   "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
  41.107  is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
  41.108 -	    'b stream => 'c stream => bool"
  41.109 +            'b stream => 'c stream => bool"
  41.110  is_g     :: "('b stream -> 'c stream) => bool"
  41.111  def_g    :: "('b stream -> 'c stream) => bool"
  41.112 -Rf	 :: 
  41.113 +Rf       :: 
  41.114  "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
  41.115  
  41.116  defs
  41.117  
  41.118 -is_f		"is_f f == (! i1 i2 o1 o2.
  41.119 -			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
  41.120 +is_f            "is_f f == (! i1 i2 o1 o2.
  41.121 +                        f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
  41.122  
  41.123 -is_net_g	"is_net_g f x y == (? z. 
  41.124 -			<y,z> = f`<x,z> &
  41.125 -			(! oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
  41.126 +is_net_g        "is_net_g f x y == (? z. 
  41.127 +                        <y,z> = f`<x,z> &
  41.128 +                        (! oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
  41.129  
  41.130 -is_g		"is_g g  == (? f.
  41.131 -			is_f f  & 
  41.132 -			(!x y. g`x = y --> is_net_g f x y))"
  41.133 +is_g            "is_g g  == (? f.
  41.134 +                        is_f f  & 
  41.135 +                        (!x y. g`x = y --> is_net_g f x y))"
  41.136  
  41.137  
  41.138 -def_g		"def_g g == (? f.
  41.139 -			is_f f  & 
  41.140 -	      		g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)))" 
  41.141 +def_g           "def_g g == (? f.
  41.142 +                        is_f f  & 
  41.143 +                        g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)))" 
  41.144  
  41.145  end
    42.1 --- a/src/HOLCF/explicit_domains/Stream.thy	Tue Feb 06 12:27:17 1996 +0100
    42.2 +++ b/src/HOLCF/explicit_domains/Stream.thy	Tue Feb 06 12:42:31 1996 +0100
    42.3 @@ -1,6 +1,6 @@
    42.4  (* 
    42.5      ID:         $Id$
    42.6 -    Author: 	Franz Regensburger
    42.7 +    Author:     Franz Regensburger
    42.8      Copyright   1993 Technische Universitaet Muenchen
    42.9  
   42.10  Theory for streams without defined empty stream 
   42.11 @@ -32,22 +32,22 @@
   42.12  (* ----------------------------------------------------------------------- *)
   42.13  (* essential constants                                                     *)
   42.14  
   42.15 -stream_rep	:: "('a stream) -> ('a ** ('a stream)u)"
   42.16 -stream_abs	:: "('a ** ('a stream)u) -> ('a stream)"
   42.17 +stream_rep      :: "('a stream) -> ('a ** ('a stream)u)"
   42.18 +stream_abs      :: "('a ** ('a stream)u) -> ('a stream)"
   42.19  
   42.20  (* ----------------------------------------------------------------------- *)
   42.21  (* abstract constants and auxiliary constants                              *)
   42.22  
   42.23 -stream_copy	:: "('a stream -> 'a stream) ->'a stream -> 'a stream"
   42.24 +stream_copy     :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
   42.25  
   42.26 -scons		:: "'a -> 'a stream -> 'a stream"
   42.27 -stream_when	:: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
   42.28 -is_scons	:: "'a stream -> tr"
   42.29 -shd		:: "'a stream -> 'a"
   42.30 -stl		:: "'a stream -> 'a stream"
   42.31 -stream_take	:: "nat => 'a stream -> 'a stream"
   42.32 -stream_finite	:: "'a stream => bool"
   42.33 -stream_bisim	:: "('a stream => 'a stream => bool) => bool"
   42.34 +scons           :: "'a -> 'a stream -> 'a stream"
   42.35 +stream_when     :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
   42.36 +is_scons        :: "'a stream -> tr"
   42.37 +shd             :: "'a stream -> 'a"
   42.38 +stl             :: "'a stream -> 'a stream"
   42.39 +stream_take     :: "nat => 'a stream -> 'a stream"
   42.40 +stream_finite   :: "'a stream => bool"
   42.41 +stream_bisim    :: "('a stream => 'a stream => bool) => bool"
   42.42  
   42.43  rules
   42.44  
   42.45 @@ -62,11 +62,11 @@
   42.46  (* stream_abs is an isomorphism with inverse stream_rep                    *)
   42.47  (* identity is the least endomorphism on 'a stream                         *)
   42.48  
   42.49 -stream_abs_iso	"stream_rep`(stream_abs`x) = x"
   42.50 -stream_rep_iso	"stream_abs`(stream_rep`x) = x"
   42.51 -stream_copy_def	"stream_copy == (LAM f. stream_abs oo 
   42.52 - 		(ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
   42.53 -stream_reach	"(fix`stream_copy)`x = x"
   42.54 +stream_abs_iso  "stream_rep`(stream_abs`x) = x"
   42.55 +stream_rep_iso  "stream_abs`(stream_rep`x) = x"
   42.56 +stream_copy_def "stream_copy == (LAM f. stream_abs oo 
   42.57 +                (ssplit`(LAM x y. (|x , (lift`(up oo f))`y|) )) oo stream_rep)"
   42.58 +stream_reach    "(fix`stream_copy)`x = x"
   42.59  
   42.60  defs
   42.61  (* ----------------------------------------------------------------------- *)
   42.62 @@ -74,7 +74,7 @@
   42.63  (* ----------------------------------------------------------------------- *)
   42.64  (* constructors                                                            *)
   42.65  
   42.66 -scons_def	"scons == (LAM x l. stream_abs`(| x, up`l |))"
   42.67 +scons_def       "scons == (LAM x l. stream_abs`(| x, up`l |))"
   42.68  
   42.69  (* ----------------------------------------------------------------------- *)
   42.70  (* discriminator functional                                                *)
   42.71 @@ -85,9 +85,9 @@
   42.72  (* ----------------------------------------------------------------------- *)
   42.73  (* discriminators and selectors                                            *)
   42.74  
   42.75 -is_scons_def	"is_scons == stream_when`(LAM x l.TT)"
   42.76 -shd_def		"shd == stream_when`(LAM x l.x)"
   42.77 -stl_def		"stl == stream_when`(LAM x l.l)"
   42.78 +is_scons_def    "is_scons == stream_when`(LAM x l.TT)"
   42.79 +shd_def         "shd == stream_when`(LAM x l.x)"
   42.80 +stl_def         "stl == stream_when`(LAM x l.l)"
   42.81  
   42.82  (* ----------------------------------------------------------------------- *)
   42.83  (* the taker for streams                                                   *)
   42.84 @@ -96,7 +96,7 @@
   42.85  
   42.86  (* ----------------------------------------------------------------------- *)
   42.87  
   42.88 -stream_finite_def	"stream_finite == (%s.? n.stream_take n `s=s)"
   42.89 +stream_finite_def       "stream_finite == (%s.? n.stream_take n `s=s)"
   42.90  
   42.91  (* ----------------------------------------------------------------------- *)
   42.92  (* definition of bisimulation is determined by domain equation             *)
   42.93 @@ -104,7 +104,7 @@
   42.94  
   42.95  stream_bisim_def "stream_bisim ==
   42.96  (%R.!s1 s2.
   42.97 - 	R s1 s2 -->
   42.98 +        R s1 s2 -->
   42.99    ((s1=UU & s2=UU) |
  42.100    (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
  42.101  
    43.1 --- a/src/HOLCF/explicit_domains/Stream2.thy	Tue Feb 06 12:27:17 1996 +0100
    43.2 +++ b/src/HOLCF/explicit_domains/Stream2.thy	Tue Feb 06 12:42:31 1996 +0100
    43.3 @@ -1,6 +1,6 @@
    43.4  (* 
    43.5      ID:         $Id$
    43.6 -    Author: 	Franz Regensburger
    43.7 +    Author:     Franz Regensburger
    43.8      Copyright   1993 Technische Universitaet Muenchen
    43.9  
   43.10  Additional constants for stream
   43.11 @@ -10,7 +10,7 @@
   43.12  
   43.13  consts
   43.14  
   43.15 -smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
   43.16 +smap            :: "('a -> 'b) -> 'a stream -> 'b stream"
   43.17  
   43.18  defs
   43.19  
   43.20 @@ -22,7 +22,7 @@
   43.21        
   43.22  
   43.23  (*
   43.24 -		smap`f`UU = UU
   43.25 +                smap`f`UU = UU
   43.26        x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
   43.27  
   43.28  *)