1.1 --- a/src/HOLCF/ROOT.ML Sat Nov 03 18:41:13 2001 +0100
1.2 +++ b/src/HOLCF/ROOT.ML Sat Nov 03 18:41:28 2001 +0100
1.3 @@ -1,10 +1,9 @@
1.4 (* Title: HOLCF/ROOT.ML
1.5 ID: $Id$
1.6 Author: Franz Regensburger
1.7 - Copyright 1993 Technische Universitaet Muenchen
1.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
1.9
1.10 -ROOT file for the conservative extension of HOL by the LCF logic.
1.11 -Should be executed in subdirectory HOLCF.
1.12 +Conservative (semantic) extension of HOL by the LCF logic.
1.13 *)
1.14
1.15 val banner = "HOLCF";
2.1 --- a/src/HOLCF/ex/Dagstuhl.ML Sat Nov 03 18:41:13 2001 +0100
2.2 +++ b/src/HOLCF/ex/Dagstuhl.ML Sat Nov 03 18:41:28 2001 +0100
2.3 @@ -1,7 +1,5 @@
2.4 (* $Id$ *)
2.5
2.6 -open Dagstuhl;
2.7 -
2.8 val YS_def2 = fix_prover2 Dagstuhl.thy YS_def "YS = y && YS";
2.9 val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = y && y && YYS";
2.10
3.1 --- a/src/HOLCF/ex/Fix2.ML Sat Nov 03 18:41:13 2001 +0100
3.2 +++ b/src/HOLCF/ex/Fix2.ML Sat Nov 03 18:41:28 2001 +0100
3.3 @@ -1,7 +1,7 @@
3.4 (* Title: HOLCF/ex/Fix2.ML
3.5 ID: $Id$
3.6 Author: Franz Regensburger
3.7 - Copyright 1995 Technische Universitaet Muenchen
3.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
3.9 *)
3.10
3.11 Goal "fix = gix";
4.1 --- a/src/HOLCF/ex/Fix2.thy Sat Nov 03 18:41:13 2001 +0100
4.2 +++ b/src/HOLCF/ex/Fix2.thy Sat Nov 03 18:41:28 2001 +0100
4.3 @@ -1,11 +1,10 @@
4.4 (* Title: HOLCF/ex/Fix2.thy
4.5 ID: $Id$
4.6 Author: Franz Regensburger
4.7 - Copyright 1995 Technische Universitaet Muenchen
4.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
4.9
4.10 - Show that fix is the unique least fixed-point operator.
4.11 - From axioms gix1_def,gix2_def it follows that fix = gix
4.12 -
4.13 +Show that fix is the unique least fixed-point operator.
4.14 +From axioms gix1_def,gix2_def it follows that fix = gix
4.15 *)
4.16
4.17 Fix2 = Fix +
5.1 --- a/src/HOLCF/ex/Focus_ex.ML Sat Nov 03 18:41:13 2001 +0100
5.2 +++ b/src/HOLCF/ex/Focus_ex.ML Sat Nov 03 18:41:28 2001 +0100
5.3 @@ -1,4 +1,3 @@
5.4 -open Focus_ex;
5.5
5.6 (* first some logical trading *)
5.7
6.1 --- a/src/HOLCF/ex/Hoare.thy Sat Nov 03 18:41:13 2001 +0100
6.2 +++ b/src/HOLCF/ex/Hoare.thy Sat Nov 03 18:41:28 2001 +0100
6.3 @@ -1,9 +1,9 @@
6.4 (* Title: HOLCF/ex/hoare.thy
6.5 ID: $Id$
6.6 Author: Franz Regensburger
6.7 - Copyright 1993 Technische Universitaet Muenchen
6.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
6.9
6.10 -Theory for an example by C.A.R. Hoare
6.11 +Theory for an example by C.A.R. Hoare
6.12
6.13 p x = if b1 x
6.14 then p (g x)
7.1 --- a/src/HOLCF/ex/Loop.ML Sat Nov 03 18:41:13 2001 +0100
7.2 +++ b/src/HOLCF/ex/Loop.ML Sat Nov 03 18:41:28 2001 +0100
7.3 @@ -1,7 +1,7 @@
7.4 (* Title: HOLCF/ex/Loop.ML
7.5 ID: $Id$
7.6 Author: Franz Regensburger
7.7 - Copyright 1993 Technische Universitaet Muenchen
7.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
7.9
7.10 Theory for a loop primitive like while
7.11 *)
8.1 --- a/src/HOLCF/ex/Loop.thy Sat Nov 03 18:41:13 2001 +0100
8.2 +++ b/src/HOLCF/ex/Loop.thy Sat Nov 03 18:41:28 2001 +0100
8.3 @@ -1,7 +1,7 @@
8.4 (* Title: HOLCF/ex/Loop.thy
8.5 ID: $Id$
8.6 Author: Franz Regensburger
8.7 - Copyright 1993 Technische Universitaet Muenchen
8.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
8.9
8.10 Theory for a loop primitive like while
8.11 *)
9.1 --- a/src/HOLCF/ex/ROOT.ML Sat Nov 03 18:41:13 2001 +0100
9.2 +++ b/src/HOLCF/ex/ROOT.ML Sat Nov 03 18:41:28 2001 +0100
9.3 @@ -1,7 +1,5 @@
9.4 (* Title: HOLCF/ex/ROOT.ML
9.5 ID: $Id$
9.6 - Author: Tobias Nipkow
9.7 - Copyright 1994 TU Muenchen
9.8
9.9 Misc HOLCF examples.
9.10 *)
10.1 --- a/src/HOLCF/ex/Stream.ML Sat Nov 03 18:41:13 2001 +0100
10.2 +++ b/src/HOLCF/ex/Stream.ML Sat Nov 03 18:41:28 2001 +0100
10.3 @@ -1,11 +1,9 @@
10.4 (* Title: HOLCF/ex//Stream.ML
10.5 ID: $Id$
10.6 - Author: Franz Regensburger, David von Oheimb
10.7 - Copyright 1993, 1995 Technische Universitaet Muenchen
10.8 - Author: David von Oheimb (major extensions)
10.9 + Author: Franz Regensburger and David von Oheimb, TU Muenchen
10.10 License: GPL (GNU GENERAL PUBLIC LICENSE)
10.11
10.12 -general Stream domain
10.13 +General Stream domain.
10.14 *)
10.15
10.16 fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
11.1 --- a/src/HOLCF/ex/Stream.thy Sat Nov 03 18:41:13 2001 +0100
11.2 +++ b/src/HOLCF/ex/Stream.thy Sat Nov 03 18:41:28 2001 +0100
11.3 @@ -1,9 +1,9 @@
11.4 (* Title: HOLCF/ex/Stream.thy
11.5 ID: $Id$
11.6 Author: Franz Regensburger, David von Oheimb
11.7 - Copyright 1993, 1995 Technische Universitaet Muenchen
11.8 + License: GPL (GNU GENERAL PUBLIC LICENSE)
11.9
11.10 -general Stream domain
11.11 +General Stream domain.
11.12 *)
11.13
11.14 Stream = HOLCF + Nat_Infinity +
11.15 @@ -12,16 +12,16 @@
11.16
11.17 consts
11.18
11.19 - smap :: "('a \\<rightarrow> 'b) \\<rightarrow> 'a stream \\<rightarrow> 'b stream"
11.20 - sfilter :: "('a \\<rightarrow> tr) \\<rightarrow> 'a stream \\<rightarrow> 'a stream"
11.21 - slen :: "'a stream \\<Rightarrow> inat" ("#_" [1000] 1000)
11.22 + smap :: "('a -> 'b) -> 'a stream -> 'b stream"
11.23 + sfilter :: "('a -> tr) -> 'a stream -> 'a stream"
11.24 + slen :: "'a stream => inat" ("#_" [1000] 1000)
11.25
11.26 defs
11.27
11.28 - smap_def "smap \\<equiv> fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
11.29 - sfilter_def "sfilter \\<equiv> fix\\<cdot>(\\<Lambda>h p s. case s of x && xs =>
11.30 + smap_def "smap == fix\\<cdot>(\\<Lambda>h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
11.31 + sfilter_def "sfilter == fix\\<cdot>(\\<Lambda>h p s. case s of x && xs =>
11.32 If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
11.33 - slen_def "#s \\<equiv> if stream_finite s
11.34 + slen_def "#s == if stream_finite s
11.35 then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"
11.36
11.37 end