--- a/src/HOLCF/Cfun1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
The type -> of continuous functions.
*)
--- a/src/HOLCF/Cfun1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Definition of the type -> of continuous functions.
--- a/src/HOLCF/Cfun2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun2
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance ->::(cpo,cpo)po
*)
--- a/src/HOLCF/Cfun2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance ->::(cpo,cpo)po
--- a/src/HOLCF/Cfun3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun3
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of -> for class pcpo
*)
--- a/src/HOLCF/Cfun3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cfun3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cfun3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of -> for class pcpo
--- a/src/HOLCF/Cont.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cont.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cont.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Results about continuity and monotonicity
*)
--- a/src/HOLCF/Cont.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cont.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/cont.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Results about continuity and monotonicity
*)
--- a/src/HOLCF/Cprod1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cprod1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial ordering for cartesian product of HOL theory Product_Type.thy
*)
--- a/src/HOLCF/Cprod1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
(* Title: HOLCF/Cprod1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial ordering for cartesian product of HOL theory prod.thy
-
*)
Cprod1 = Cfun3 +
--- a/src/HOLCF/Cprod2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cprod2
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance *::(pcpo,pcpo)po
*)
--- a/src/HOLCF/Cprod2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cprod2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance *::(pcpo,pcpo)po
--- a/src/HOLCF/Cprod3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cprod3
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of * for class pcpo and cpo.
*)
--- a/src/HOLCF/Cprod3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Cprod3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Cprod3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of * for class pcpo and cpo.
*)
--- a/src/HOLCF/Discrete.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Discrete.ML
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
Goalw [undiscr_def] "undiscr(Discr x) = x";
--- a/src/HOLCF/Discrete.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/Discrete.thy
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Discrete CPOs
+Discrete CPOs.
*)
Discrete = Discrete1 +
--- a/src/HOLCF/Discrete0.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete0.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Discrete0.ML
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Proves that 'a discr is a po
*)
--- a/src/HOLCF/Discrete0.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete0.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/Discrete0.thy
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Discrete CPOs
+Discrete CPOs.
*)
Discrete0 = Cont + Datatype +
--- a/src/HOLCF/Discrete1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Discrete1.ML
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Proves that 'a discr is a cpo
*)
--- a/src/HOLCF/Discrete1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Discrete1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/Discrete1.thy
ID: $Id$
Author: Tobias Nipkow
- Copyright 1997 TUM
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Discrete CPOs
+Discrete CPOs.
*)
Discrete1 = Discrete0 +
--- a/src/HOLCF/Fix.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fix.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Fix.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
fixed point operator and admissibility
*)
--- a/src/HOLCF/Fix.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fix.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
(* Title: HOLCF/Fix.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
definitions for fixed point operator and admissibility
-
*)
Fix = Cfun3 +
--- a/src/HOLCF/Fun1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Fun1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Definition of the partial ordering for the type of all functions => (fun)
*)
--- a/src/HOLCF/Fun1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,13 +1,11 @@
(* Title: HOLCF/Fun1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Definition of the partial ordering for the type of all functions => (fun)
REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
-
*)
Fun1 = Pcpo +
--- a/src/HOLCF/Fun2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Fun2.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance =>::(term,po)po
*)
--- a/src/HOLCF/Fun2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Fun2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance =>::(term,po)po
*)
--- a/src/HOLCF/Fun3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Fun3.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
(* for compatibility with old HOLCF-Version *)
--- a/src/HOLCF/Fun3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Fun3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/Fun3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of => (fun) for class pcpo
-
*)
Fun3 = Fun2 +
--- a/src/HOLCF/HOLCF.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/HOLCF.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/HOLCF.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
use"adm.ML";
--- a/src/HOLCF/HOLCF.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/HOLCF.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
(* Title: HOLCF/HOLCF.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Top theory for HOLCF system
-
+Top theory for HOLCF system.
*)
HOLCF = Sprod3 + Ssum3 + Up3 + Lift + Discrete + One + Tr
--- a/src/HOLCF/One.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/One.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/One.ML
ID: $Id$
Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-The unit domain
+The unit domain.
*)
(* ------------------------------------------------------------------------ *)
@@ -11,7 +11,7 @@
(* ------------------------------------------------------------------------ *)
Goalw [ONE_def] "t=UU | t = ONE";
-by (lift.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (Simp_tac 1);
by (Simp_tac 1);
qed "Exh_one";
--- a/src/HOLCF/One.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/One.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/One.thy
ID: $Id$
Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
One = Lift +
--- a/src/HOLCF/Pcpo.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Pcpo.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Pcpo.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
introduction of the classes cpo and pcpo
*)
--- a/src/HOLCF/Pcpo.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Pcpo.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Pcpo.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
introduction of the classes cpo and pcpo
*)
--- a/src/HOLCF/Porder.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Porder
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Conservative extension of theory Porder0 by constant definitions
*)
--- a/src/HOLCF/Porder.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/porder.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Conservative extension of theory Porder0 by constant definitions
-
*)
Porder = Porder0 +
--- a/src/HOLCF/Porder0.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder0.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/Porder0.ML
ID: $Id$
Author: Oscar Slotosch
- Copyright 1997 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
- derive the characteristic axioms for the characteristic constants
+derive the characteristic axioms for the characteristic constants
*)
AddIffs [refl_less];
--- a/src/HOLCF/Porder0.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Porder0.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/Porder0.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Definition of class porder (partial order)
-
+Definition of class porder (partial order).
*)
Porder0 = Main +
--- a/src/HOLCF/Sprod0.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod0.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Sprod0
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Strict product with typedef.
*)
--- a/src/HOLCF/Sprod0.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod0.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Sprod0.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Strict product with typedef.
*)
--- a/src/HOLCF/Sprod1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,8 +1,7 @@
(* Title: HOLCF/Sprod1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Sprod1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/sprod1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Partial ordering for the strict product
+Partial ordering for the strict product.
*)
Sprod1 = Sprod0 +
--- a/src/HOLCF/Sprod2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Sprod2.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance **::(pcpo,pcpo)po
*)
--- a/src/HOLCF/Sprod2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Sprod2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance **::(pcpo,pcpo)po
*)
--- a/src/HOLCF/Sprod3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Sprod3
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ** for class pcpo
*)
--- a/src/HOLCF/Sprod3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Sprod3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/sprod3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ** for class pcpo
*)
--- a/src/HOLCF/Ssum0.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum0.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum0.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Strict sum with typedef
*)
--- a/src/HOLCF/Ssum0.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum0.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum0.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Strict sum with typedef
*)
--- a/src/HOLCF/Ssum1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial ordering for the strict sum ++
*)
--- a/src/HOLCF/Ssum1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Partial ordering for the strict sum ++
*)
--- a/src/HOLCF/Ssum2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum2.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance ++::(pcpo,pcpo)po
*)
--- a/src/HOLCF/Ssum2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/ssum2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance ++::(pcpo,pcpo)po
*)
--- a/src/HOLCF/Ssum3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Ssum3.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ++ for class pcpo
*)
--- a/src/HOLCF/Ssum3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Ssum3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/ssum3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ++ for class pcpo
*)
--- a/src/HOLCF/Tr.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Tr.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Tr.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
*)
@@ -11,7 +11,7 @@
(* ------------------------------------------------------------------------ *)
Goalw [FF_def,TT_def] "t=UU | t = TT | t = FF";
-by (lift.induct_tac "t" 1);
+by (induct_tac "t" 1);
by (fast_tac HOL_cs 1);
by (fast_tac (HOL_cs addss simpset()) 1);
qed "Exh_tr";
--- a/src/HOLCF/Tr.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Tr.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Tr.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
*)
--- a/src/HOLCF/Up1.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up1.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/Up1.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Lifting
+Lifting.
*)
Goal "Rep_Up (Abs_Up y) = y";
--- a/src/HOLCF/Up1.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up1.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
(* Title: HOLCF/Up1.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-Lifting
-
+Lifting.
*)
Up1 = Cfun3 + Sum_Type + Datatype +
--- a/src/HOLCF/Up2.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up2.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Up2.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance u::(pcpo)po
*)
--- a/src/HOLCF/Up2.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up2.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,10 +1,9 @@
(* Title: HOLCF/Up2.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class Instance u::(pcpo)po
-
*)
Up2 = Up1 +
--- a/src/HOLCF/Up3.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up3.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/Up3.ML
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ('a)u for class pcpo
*)
--- a/src/HOLCF/Up3.thy Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/Up3.thy Sat Nov 03 01:41:26 2001 +0100
@@ -1,11 +1,9 @@
(* Title: HOLCF/Up3.thy
ID: $Id$
Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ('a)u for class pcpo
-
*)
Up3 = Up2 +
--- a/src/HOLCF/cont_consts.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/cont_consts.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,6 +1,7 @@
(* Title: HOLCF/cont_consts.ML
ID: $Id$
Author: Tobias Mayr and David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Theory extender for consts section.
*)
--- a/src/HOLCF/domain/axioms.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/axioms.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/domain/axioms.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-syntax generator for domain section
+Syntax generator for domain section.
*)
structure Domain_Axioms = struct
--- a/src/HOLCF/domain/extender.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/extender.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,7 +1,7 @@
(* Title: HOLCF/domain/extender.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Theory extender for domain section.
*)
--- a/src/HOLCF/domain/interface.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/interface.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/domain/interface.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-parser for domain section
+Parser for domain section.
*)
local
--- a/src/HOLCF/domain/library.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/library.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/domain/library.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-library for domain section
+Library for domain section.
*)
--- a/src/HOLCF/domain/syntax.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/syntax.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/domain/syntax.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-syntax generator for domain section
+Syntax generator for domain section.
*)
structure Domain_Syntax = struct
--- a/src/HOLCF/domain/theorems.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/domain/theorems.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/domain/theorems.ML
ID: $Id$
- Author : David von Oheimb
- Copyright 1995, 1996 TU Muenchen
+ Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
-proof generator for domain section
+Proof generator for domain section.
*)
--- a/src/HOLCF/holcf_logic.ML Sat Nov 03 01:40:28 2001 +0100
+++ b/src/HOLCF/holcf_logic.ML Sat Nov 03 01:41:26 2001 +0100
@@ -1,6 +1,7 @@
(* Title: HOLCF/holcf_logic.ML
ID: $Id$
Author: David von Oheimb
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Abstract syntax operations for HOLCF.
*)
@@ -31,11 +32,7 @@
structure HOLCFLogic: HOLCF_LOGIC =
struct
-local
-
- open HOLogic;
-
-in
+open HOLogic;
fun mk_btyp t (S,T) = Type (t,[S,T]);
val mk_prodT = mk_btyp "*";
@@ -62,5 +59,4 @@
val oneT = Type (intern "one",[ ]);
end;
-end; (* local *)
-end; (* struct *)
+end;