# HG changeset patch
# User wenzelm
# Date 1004809288 -3600
# Node ID 49f6c49454c210e615ade3919f066f3e95ea10bc
# Parent  f2ee4b5d02f249a0cfb02b71ef88c05e270b2314
GPLed;

diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ROOT.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,10 +1,9 @@
 (*  Title:      HOLCF/ROOT.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-ROOT file for the conservative extension of HOL by the LCF logic.
-Should be executed in subdirectory HOLCF.
+Conservative (semantic) extension of HOL by the LCF logic.
 *)
 
 val banner = "HOLCF";
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Dagstuhl.ML
--- a/src/HOLCF/ex/Dagstuhl.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Dagstuhl.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,7 +1,5 @@
 (* $Id$ *)
 
-open Dagstuhl;
-
 val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = y && YS";
 val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = y && y && YYS";
 
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Fix2.ML
--- a/src/HOLCF/ex/Fix2.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Fix2.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/ex/Fix2.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 Goal "fix = gix";
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Fix2.thy
--- a/src/HOLCF/ex/Fix2.thy	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Fix2.thy	Sat Nov 03 18:41:28 2001 +0100
@@ -1,11 +1,10 @@
 (*  Title:      HOLCF/ex/Fix2.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1995 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
- Show that fix is the unique least fixed-point operator. 
- From axioms gix1_def,gix2_def it follows that fix = gix
-
+Show that fix is the unique least fixed-point operator. 
+From axioms gix1_def,gix2_def it follows that fix = gix
 *)
 
 Fix2 = Fix + 
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Focus_ex.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,4 +1,3 @@
-open Focus_ex;
 
 (* first some logical trading *)
 
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Hoare.thy	Sat Nov 03 18:41:28 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/ex/hoare.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Theory for an example by C.A.R. Hoare 
+Theory for an example by C.A.R. Hoare
 
 p x = if b1 x 
          then p (g x)
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Loop.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/ex/Loop.ML
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory for a loop primitive like while
 *)
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Loop.thy	Sat Nov 03 18:41:28 2001 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOLCF/ex/Loop.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory for a loop primitive like while
 *)
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/ROOT.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOLCF/ex/ROOT.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1994 TU Muenchen
 
 Misc HOLCF examples.
 *)
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Stream.ML	Sat Nov 03 18:41:28 2001 +0100
@@ -1,11 +1,9 @@
 (*  Title: 	HOLCF/ex//Stream.ML
     ID:         $Id$
-    Author: 	Franz Regensburger, David von Oheimb
-    Copyright   1993, 1995 Technische Universitaet Muenchen
-    Author: 	David von Oheimb (major extensions)
+    Author: 	Franz Regensburger and David von Oheimb, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-general Stream domain
+General Stream domain.
 *)
 
 fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
diff -r f2ee4b5d02f2 -r 49f6c49454c2 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Sat Nov 03 18:41:13 2001 +0100
+++ b/src/HOLCF/ex/Stream.thy	Sat Nov 03 18:41:28 2001 +0100
@@ -1,9 +1,9 @@
 (*  Title: 	HOLCF/ex/Stream.thy
     ID:         $Id$
     Author: 	Franz Regensburger, David von Oheimb
-    Copyright   1993, 1995 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-general Stream domain
+General Stream domain.
 *)
 
 Stream = HOLCF + Nat_Infinity +
@@ -12,16 +12,16 @@
 
 consts
 
-  smap		:: "('a \\<rightarrow> 'b) \\<rightarrow> 'a stream \\<rightarrow> 'b stream"
-  sfilter	:: "('a \\<rightarrow> tr) \\<rightarrow> 'a stream \\<rightarrow> 'a stream"
-  slen		:: "'a stream \\<Rightarrow> inat"			("#_" [1000] 1000)
+  smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
+  sfilter	:: "('a -> tr) -> 'a stream -> 'a stream"
+  slen		:: "'a stream => inat"			("#_" [1000] 1000)
 
 defs
 
-  smap_def	"smap	 \\<equiv> fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
-  sfilter_def	"sfilter \\<equiv> fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => 
+  smap_def	"smap	 == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
+  sfilter_def	"sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs => 
 				     If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
-  slen_def	"#s \\<equiv> if stream_finite s 
+  slen_def	"#s == if stream_finite s 
 		      then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"
 
 end