new header syntax;
authorwenzelm
Wed Sep 21 18:04:49 2005 +0200 (2005-09-21)
changeset 17566484ff733f29c
parent 17565 7322f37d3344
child 17567 20c0b69dd192
new header syntax;
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Prob.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/Generate-HOL/GenHOL4Vec.thy
src/HOL/Import/Generate-HOL/GenHOL4Word32.thy
src/HOL/Import/HOL/HOL4Base.thy
src/HOL/Import/HOL/HOL4Prob.thy
src/HOL/Import/HOL/HOL4Real.thy
src/HOL/Import/HOL/HOL4Vec.thy
src/HOL/Import/HOL/HOL4Word32.thy
     1.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Sep 21 17:25:32 2005 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Sep 21 18:04:49 2005 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  setup_dump "../HOL" "HOL4Base";
     1.6  
     1.7 -append_dump {*theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":*};
     1.8 +append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};
     1.9  
    1.10  import_theory bool;
    1.11  
     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Wed Sep 21 17:25:32 2005 +0200
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy	Wed Sep 21 18:04:49 2005 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  setup_dump "../HOL" "HOL4Prob";
     2.6  
     2.7 -append_dump "theory HOL4Prob = HOL4Real:";
     2.8 +append_dump "theory HOL4Prob imports HOL4Real begin";
     2.9  
    2.10  import_theory prob_extra;
    2.11  
     3.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 21 17:25:32 2005 +0200
     3.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Sep 21 18:04:49 2005 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  setup_dump "../HOL" "HOL4Real";
     3.6  
     3.7 -append_dump "theory HOL4Real = HOL4Base:";
     3.8 +append_dump "theory HOL4Real imports HOL4Base begin";
     3.9  
    3.10  import_theory realax;
    3.11  
     4.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Wed Sep 21 17:25:32 2005 +0200
     4.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy	Wed Sep 21 18:04:49 2005 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  setup_dump "../HOL" "HOL4Vec";
     4.6  
     4.7 -append_dump "theory HOL4Vec = HOL4Base:";
     4.8 +append_dump "theory HOL4Vec imports HOL4Base begin";
     4.9  
    4.10  import_theory res_quan;
    4.11  end_import;
     5.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Wed Sep 21 17:25:32 2005 +0200
     5.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy	Wed Sep 21 18:04:49 2005 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  setup_dump "../HOL" "HOL4Word32";
     5.6  
     5.7 -append_dump "theory HOL4Word32 = HOL4Base:";
     5.8 +append_dump "theory HOL4Word32 imports HOL4Base begin";
     5.9  
    5.10  import_theory bits;
    5.11  
     6.1 --- a/src/HOL/Import/HOL/HOL4Base.thy	Wed Sep 21 17:25:32 2005 +0200
     6.2 +++ b/src/HOL/Import/HOL/HOL4Base.thy	Wed Sep 21 18:04:49 2005 +0200
     6.3 @@ -1,6 +1,6 @@
     6.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     6.5  
     6.6 -theory HOL4Base = "../HOL4Compat" + "../HOL4Syntax":
     6.7 +theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
     6.8  
     6.9  ;setup_theory bool
    6.10  
     7.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 21 17:25:32 2005 +0200
     7.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 21 18:04:49 2005 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     7.5  
     7.6 -theory HOL4Prob = HOL4Real:
     7.7 +theory HOL4Prob imports HOL4Real begin
     7.8  
     7.9  ;setup_theory prob_extra
    7.10  
     8.1 --- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 21 17:25:32 2005 +0200
     8.2 +++ b/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 21 18:04:49 2005 +0200
     8.3 @@ -1,6 +1,6 @@
     8.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     8.5  
     8.6 -theory HOL4Real = HOL4Base:
     8.7 +theory HOL4Real imports HOL4Base begin
     8.8  
     8.9  ;setup_theory realax
    8.10  
     9.1 --- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 21 17:25:32 2005 +0200
     9.2 +++ b/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 21 18:04:49 2005 +0200
     9.3 @@ -1,6 +1,6 @@
     9.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     9.5  
     9.6 -theory HOL4Vec = HOL4Base:
     9.7 +theory HOL4Vec imports HOL4Base begin
     9.8  
     9.9  ;setup_theory res_quan
    9.10  
    10.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 21 17:25:32 2005 +0200
    10.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 21 18:04:49 2005 +0200
    10.3 @@ -1,6 +1,6 @@
    10.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
    10.5  
    10.6 -theory HOL4Word32 = HOL4Base:
    10.7 +theory HOL4Word32 imports HOL4Base begin
    10.8  
    10.9  ;setup_theory bits
   10.10