--- 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";
--- 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";
--- 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";
--- 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 +
--- 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 *)
--- 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)
--- 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
*)
--- 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
*)
--- 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.
*)
--- 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
--- 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