explicit locations for import_theory and setup_theory, for better user interface conformance
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Mar 03 21:00:04 2012 +0100
@@ -10,7 +10,7 @@
append_dump {*theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin*};
-import_theory bool;
+import_theory "~~/src/HOL/Import/HOL" bool;
type_maps
bool > HOL.bool;
@@ -39,14 +39,14 @@
end_import;
-import_theory combin;
+import_theory "~~/src/HOL/Import/HOL" combin;
const_maps
o > Fun.comp;
end_import;
-import_theory sum;
+import_theory "~~/src/HOL/Import/HOL" sum;
type_maps
sum > Sum_Type.sum;
@@ -70,7 +70,7 @@
end_import;
-import_theory one;
+import_theory "~~/src/HOL/Import/HOL" one;
type_maps
one > Product_Type.unit;
@@ -86,7 +86,7 @@
end_import;
-import_theory option;
+import_theory "~~/src/HOL/Import/HOL" option;
type_maps
option > Option.option;
@@ -111,17 +111,17 @@
end_import;
-import_theory marker;
+import_theory "~~/src/HOL/Import/HOL" marker;
end_import;
-import_theory relation;
+import_theory "~~/src/HOL/Import/HOL" relation;
const_renames
reflexive > pred_reflexive;
end_import;
-import_theory pair;
+import_theory "~~/src/HOL/Import/HOL" pair;
type_maps
prod > Product_Type.prod;
@@ -144,7 +144,7 @@
end_import;
-import_theory num;
+import_theory "~~/src/HOL/Import/HOL" num;
type_maps
num > Nat.nat;
@@ -164,14 +164,14 @@
end_import;
-import_theory prim_rec;
+import_theory "~~/src/HOL/Import/HOL" prim_rec;
const_maps
"<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
end_import;
-import_theory arithmetic;
+import_theory "~~/src/HOL/Import/HOL" arithmetic;
const_maps
ALT_ZERO > HOL4Compat.ALT_ZERO
@@ -194,29 +194,29 @@
end_import;
-import_theory hrat;
+import_theory "~~/src/HOL/Import/HOL" hrat;
end_import;
-import_theory hreal;
+import_theory "~~/src/HOL/Import/HOL" hreal;
end_import;
-import_theory numeral;
+import_theory "~~/src/HOL/Import/HOL" numeral;
end_import;
-import_theory ind_type;
+import_theory "~~/src/HOL/Import/HOL" ind_type;
end_import;
-import_theory divides;
+import_theory "~~/src/HOL/Import/HOL" divides;
const_maps
divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
end_import;
-import_theory prime;
+import_theory "~~/src/HOL/Import/HOL" prime;
end_import;
-import_theory list;
+import_theory "~~/src/HOL/Import/HOL" list;
type_maps
list > List.list;
@@ -258,16 +258,16 @@
end_import;
-import_theory pred_set;
+import_theory "~~/src/HOL/Import/HOL" pred_set;
end_import;
-import_theory operator;
+import_theory "~~/src/HOL/Import/HOL" operator;
end_import;
-import_theory rich_list;
+import_theory "~~/src/HOL/Import/HOL" rich_list;
end_import;
-import_theory state_transformer;
+import_theory "~~/src/HOL/Import/HOL" state_transformer;
end_import;
append_dump "end";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy Sat Mar 03 21:00:04 2012 +0100
@@ -10,32 +10,32 @@
append_dump "theory HOL4Prob imports HOL4Real begin";
-import_theory prob_extra;
+import_theory "~~/src/HOL/Import/HOL" prob_extra;
const_moves
COMPL > GenHOL4Base.pred_set.COMPL;
end_import;
-import_theory prob_canon;
+import_theory "~~/src/HOL/Import/HOL" prob_canon;
end_import;
-import_theory boolean_sequence;
+import_theory "~~/src/HOL/Import/HOL" boolean_sequence;
end_import;
-import_theory prob_algebra;
+import_theory "~~/src/HOL/Import/HOL" prob_algebra;
end_import;
-import_theory prob;
+import_theory "~~/src/HOL/Import/HOL" prob;
end_import;
-import_theory prob_pseudo;
+import_theory "~~/src/HOL/Import/HOL" prob_pseudo;
end_import;
-import_theory prob_indep;
+import_theory "~~/src/HOL/Import/HOL" prob_indep;
end_import;
-import_theory prob_uniform;
+import_theory "~~/src/HOL/Import/HOL" prob_uniform;
end_import;
append_dump "end";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy Sat Mar 03 21:00:04 2012 +0100
@@ -10,7 +10,7 @@
append_dump "theory HOL4Real imports HOL4Base begin";
-import_theory realax;
+import_theory "~~/src/HOL/Import/HOL" realax;
type_maps
real > RealDef.real;
@@ -49,7 +49,7 @@
end_import;
-import_theory real;
+import_theory "~~/src/HOL/Import/HOL" real;
const_maps
real_gt > HOL4Compat.real_gt
@@ -63,28 +63,28 @@
end_import;
-import_theory topology;
+import_theory "~~/src/HOL/Import/HOL" topology;
end_import;
-import_theory nets;
+import_theory "~~/src/HOL/Import/HOL" nets;
end_import;
-import_theory seq;
+import_theory "~~/src/HOL/Import/HOL" seq;
const_renames
"-->" > "hol4-->";
end_import;
-import_theory lim;
+import_theory "~~/src/HOL/Import/HOL" lim;
end_import;
-import_theory powser;
+import_theory "~~/src/HOL/Import/HOL" powser;
end_import;
-import_theory transc;
+import_theory "~~/src/HOL/Import/HOL" transc;
end_import;
-import_theory poly;
+import_theory "~~/src/HOL/Import/HOL" poly;
end_import;
append_dump "end";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Vec.thy Sat Mar 03 21:00:04 2012 +0100
@@ -10,29 +10,29 @@
append_dump "theory HOL4Vec imports HOL4Base begin";
-import_theory res_quan;
+import_theory "~~/src/HOL/Import/HOL" res_quan;
end_import;
-import_theory word_base;
+import_theory "~~/src/HOL/Import/HOL" word_base;
const_renames
BIT > bit;
end_import;
-import_theory word_num;
+import_theory "~~/src/HOL/Import/HOL" word_num;
end_import;
-import_theory word_bitop;
+import_theory "~~/src/HOL/Import/HOL" word_bitop;
end_import;
-import_theory bword_num;
+import_theory "~~/src/HOL/Import/HOL" bword_num;
end_import;
-import_theory bword_arith;
+import_theory "~~/src/HOL/Import/HOL" bword_arith;
end_import;
-import_theory bword_bitop;
+import_theory "~~/src/HOL/Import/HOL" bword_bitop;
end_import;
append_dump "end";
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Mar 03 21:00:04 2012 +0100
@@ -10,14 +10,14 @@
append_dump "theory HOL4Word32 imports HOL4Base begin";
-import_theory bits;
+import_theory "~~/src/HOL/Import/HOL" bits;
const_renames
BIT > bit
end_import;
-import_theory word32;
+import_theory "~~/src/HOL/Import/HOL" word32;
const_renames
"==" > EQUIV;
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Mar 03 21:00:04 2012 +0100
@@ -11,7 +11,7 @@
;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *}
-;import_theory hollight
+import_theory "~~/src/HOL/Import/HOLLight" hollight
;ignore_thms
(* Unit type *)
--- a/src/HOL/Import/HOL/HOL4Base.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Base.thy Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin
-;setup_theory bool
+setup_theory "~~/src/HOL/Import/HOL" bool
definition
ARB :: "'a" where
@@ -205,7 +205,7 @@
;end_setup
-;setup_theory combin
+setup_theory "~~/src/HOL/Import/HOL" combin
definition
K :: "'a => 'b => 'a" where
@@ -260,7 +260,7 @@
;end_setup
-;setup_theory sum
+setup_theory "~~/src/HOL/Import/HOL" sum
lemma ISL_OR_ISR: "ISL x | ISR x"
sorry
@@ -279,11 +279,11 @@
;end_setup
-;setup_theory one
+setup_theory "~~/src/HOL/Import/HOL" one
;end_setup
-;setup_theory option
+setup_theory "~~/src/HOL/Import/HOL" option
lemma option_CLAUSES: "(op &::bool => bool => bool)
((All::('a::type => bool) => bool)
@@ -477,7 +477,7 @@
;end_setup
-;setup_theory marker
+setup_theory "~~/src/HOL/Import/HOL" marker
consts
stmarker :: "'a => 'a"
@@ -510,7 +510,7 @@
;end_setup
-;setup_theory relation
+setup_theory "~~/src/HOL/Import/HOL" relation
definition
TC :: "('a => 'a => bool) => 'a => 'a => bool" where
@@ -758,7 +758,7 @@
;end_setup
-;setup_theory pair
+setup_theory "~~/src/HOL/Import/HOL" pair
lemma CURRY_ONE_ONE_THM: "(curry f = curry g) = (f = g)"
sorry
@@ -821,11 +821,11 @@
;end_setup
-;setup_theory num
+setup_theory "~~/src/HOL/Import/HOL" num
;end_setup
-;setup_theory prim_rec
+setup_theory "~~/src/HOL/Import/HOL" prim_rec
lemma LESS_0_0: "0 < Suc 0"
sorry
@@ -953,7 +953,7 @@
;end_setup
-;setup_theory arithmetic
+setup_theory "~~/src/HOL/Import/HOL" arithmetic
definition
nat_elim__magic :: "nat => nat" where
@@ -1347,7 +1347,7 @@
;end_setup
-;setup_theory hrat
+setup_theory "~~/src/HOL/Import/HOL" hrat
definition
trat_1 :: "nat * nat" where
@@ -1558,7 +1558,7 @@
;end_setup
-;setup_theory hreal
+setup_theory "~~/src/HOL/Import/HOL" hreal
definition
hrat_lt :: "hrat => hrat => bool" where
@@ -1842,7 +1842,7 @@
;end_setup
-;setup_theory numeral
+setup_theory "~~/src/HOL/Import/HOL" numeral
lemma numeral_suc: "Suc ALT_ZERO = NUMERAL_BIT1 ALT_ZERO &
(ALL x. Suc (NUMERAL_BIT1 x) = NUMERAL_BIT2 x) &
@@ -2069,7 +2069,7 @@
;end_setup
-;setup_theory ind_type
+setup_theory "~~/src/HOL/Import/HOL" ind_type
lemma INJ_INVERSE2: "(!!(x1::'A) (y1::'B) (x2::'A) y2::'B.
((P::'A => 'B => 'C) x1 y1 = P x2 y2) = (x1 = x2 & y1 = y2))
@@ -2304,7 +2304,7 @@
;end_setup
-;setup_theory divides
+setup_theory "~~/src/HOL/Import/HOL" divides
lemma DIVIDES_FACT: "0 < b ==> b dvd FACT b"
sorry
@@ -2314,7 +2314,7 @@
;end_setup
-;setup_theory prime
+setup_theory "~~/src/HOL/Import/HOL" prime
consts
prime :: "nat => bool"
@@ -2333,7 +2333,7 @@
;end_setup
-;setup_theory list
+setup_theory "~~/src/HOL/Import/HOL" list
consts
EL :: "nat => 'a list => 'a"
@@ -2495,7 +2495,7 @@
;end_setup
-;setup_theory pred_set
+setup_theory "~~/src/HOL/Import/HOL" pred_set
lemma EXTENSION: "(s = t) = (ALL x. IN x s = IN x t)"
sorry
@@ -3437,7 +3437,7 @@
;end_setup
-;setup_theory operator
+setup_theory "~~/src/HOL/Import/HOL" operator
definition
ASSOC :: "('a => 'a => 'a) => bool" where
@@ -3498,7 +3498,7 @@
;end_setup
-;setup_theory rich_list
+setup_theory "~~/src/HOL/Import/HOL" rich_list
consts
SNOC :: "'a => 'a list => 'a list"
@@ -4412,7 +4412,7 @@
;end_setup
-;setup_theory state_transformer
+setup_theory "~~/src/HOL/Import/HOL" state_transformer
definition
UNIT :: "'b => 'a => 'b * 'a" where
--- a/src/HOL/Import/HOL/HOL4Prob.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Prob.thy Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
theory HOL4Prob imports HOL4Real begin
-;setup_theory prob_extra
+setup_theory "~~/src/HOL/Import/HOL" prob_extra
lemma BOOL_BOOL_CASES_THM: "f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
by (import prob_extra BOOL_BOOL_CASES_THM)
@@ -213,7 +213,7 @@
;end_setup
-;setup_theory prob_canon
+setup_theory "~~/src/HOL/Import/HOL" prob_canon
consts
alg_twin :: "bool list => bool list => bool"
@@ -725,7 +725,7 @@
;end_setup
-;setup_theory boolean_sequence
+setup_theory "~~/src/HOL/Import/HOL" boolean_sequence
consts
SHD :: "(nat => bool) => bool"
@@ -802,7 +802,7 @@
;end_setup
-;setup_theory prob_algebra
+setup_theory "~~/src/HOL/Import/HOL" prob_algebra
consts
alg_embed :: "bool list => (nat => bool) => bool"
@@ -948,7 +948,7 @@
;end_setup
-;setup_theory prob
+setup_theory "~~/src/HOL/Import/HOL" prob
consts
alg_measure :: "bool list list => real"
@@ -1121,7 +1121,7 @@
;end_setup
-;setup_theory prob_pseudo
+setup_theory "~~/src/HOL/Import/HOL" prob_pseudo
consts
pseudo_linear_hd :: "nat => bool"
@@ -1203,7 +1203,7 @@
;end_setup
-;setup_theory prob_indep
+setup_theory "~~/src/HOL/Import/HOL" prob_indep
consts
indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool"
@@ -1388,7 +1388,7 @@
;end_setup
-;setup_theory prob_uniform
+setup_theory "~~/src/HOL/Import/HOL" prob_uniform
consts
unif_bound :: "nat => nat"
--- a/src/HOL/Import/HOL/HOL4Real.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Real.thy Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
theory HOL4Real imports HOL4Base begin
-;setup_theory realax
+setup_theory "~~/src/HOL/Import/HOL" realax
lemma HREAL_RDISTRIB: "hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"
by (import realax HREAL_RDISTRIB)
@@ -223,7 +223,7 @@
;end_setup
-;setup_theory real
+setup_theory "~~/src/HOL/Import/HOL" real
lemma REAL_0: "(0::real) = (0::real)"
by (import real REAL_0)
@@ -621,7 +621,7 @@
;end_setup
-;setup_theory topology
+setup_theory "~~/src/HOL/Import/HOL" topology
definition
re_Union :: "(('a => bool) => bool) => 'a => bool" where
@@ -895,7 +895,7 @@
;end_setup
-;setup_theory nets
+setup_theory "~~/src/HOL/Import/HOL" nets
definition
dorder :: "('a => 'a => bool) => bool" where
@@ -1057,7 +1057,7 @@
;end_setup
-;setup_theory seq
+setup_theory "~~/src/HOL/Import/HOL" seq
consts
"hol4-->" :: "(nat => real) => real => bool" ("hol4-->")
@@ -1338,7 +1338,7 @@
;end_setup
-;setup_theory lim
+setup_theory "~~/src/HOL/Import/HOL" lim
definition
tends_real_real :: "(real => real) => real => real => bool" where
@@ -1626,7 +1626,7 @@
;end_setup
-;setup_theory powser
+setup_theory "~~/src/HOL/Import/HOL" powser
lemma POWDIFF_LEMMA: "real.sum (0, Suc n) (%p. x ^ p * y ^ (Suc n - p)) =
y * real.sum (0, Suc n) (%p. x ^ p * y ^ (n - p))"
@@ -1711,7 +1711,7 @@
;end_setup
-;setup_theory transc
+setup_theory "~~/src/HOL/Import/HOL" transc
consts
exp :: "real => real"
@@ -2553,7 +2553,7 @@
;end_setup
-;setup_theory poly
+setup_theory "~~/src/HOL/Import/HOL" poly
consts
poly :: "real list => real => real"
--- a/src/HOL/Import/HOL/HOL4Vec.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
theory HOL4Vec imports HOL4Base begin
-;setup_theory res_quan
+setup_theory "~~/src/HOL/Import/HOL" res_quan
lemma RES_FORALL_CONJ_DIST: "RES_FORALL P (%i. Q i & R i) = (RES_FORALL P Q & RES_FORALL P R)"
by (import res_quan RES_FORALL_CONJ_DIST)
@@ -89,7 +89,7 @@
;end_setup
-;setup_theory word_base
+setup_theory "~~/src/HOL/Import/HOL" word_base
typedef (open) ('a) word = "{x. ALL word.
(ALL a0. (EX a. a0 = CONSTR 0 a (%n. BOTTOM)) --> word a0) -->
@@ -403,7 +403,7 @@
;end_setup
-;setup_theory word_num
+setup_theory "~~/src/HOL/Import/HOL" word_num
definition
LVAL :: "('a => nat) => nat => 'a list => nat" where
@@ -479,7 +479,7 @@
;end_setup
-;setup_theory word_bitop
+setup_theory "~~/src/HOL/Import/HOL" word_bitop
consts
PBITOP :: "('a word => 'b word) => bool"
@@ -766,7 +766,7 @@
;end_setup
-;setup_theory bword_num
+setup_theory "~~/src/HOL/Import/HOL" bword_num
definition
BV :: "bool => nat" where
@@ -919,7 +919,7 @@
;end_setup
-;setup_theory bword_arith
+setup_theory "~~/src/HOL/Import/HOL" bword_arith
consts
ACARRY :: "nat => bool word => bool word => bool => bool"
@@ -1053,7 +1053,7 @@
;end_setup
-;setup_theory bword_bitop
+setup_theory "~~/src/HOL/Import/HOL" bword_bitop
consts
WNOT :: "bool word => bool word"
--- a/src/HOL/Import/HOL/HOL4Word32.thy Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/HOL/HOL4Word32.thy Sat Mar 03 21:00:04 2012 +0100
@@ -2,7 +2,7 @@
theory HOL4Word32 imports HOL4Base begin
-;setup_theory bits
+setup_theory "~~/src/HOL/Import/HOL" bits
consts
DIV2 :: "nat => nat"
@@ -285,7 +285,7 @@
;end_setup
-;setup_theory word32
+setup_theory "~~/src/HOL/Import/HOL" word32
consts
HB :: "nat"
--- a/src/HOL/Import/import_syntax.ML Sat Mar 03 14:04:49 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML Sat Mar 03 21:00:04 2012 +0100
@@ -30,11 +30,11 @@
val import_segment = Parse.name >> set_import_segment
-val import_theory = Parse.name >> (fn thyname =>
+val import_theory = (Parse.name -- Parse.name) >> (fn (location, thyname) =>
fn thy =>
thy |> set_generating_thy thyname
|> Sign.add_path thyname
- |> add_dump (";setup_theory " ^ thyname))
+ |> add_dump ("setup_theory " ^ quote location ^ " " ^ thyname))
fun end_import toks =
Scan.succeed
@@ -122,9 +122,10 @@
| (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol true isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
-fun import_thy s =
+fun import_thy location s =
let
- val is = TextIO.openIn(s ^ ".imp")
+ val src_location = Path.append (Path.explode location) (Path.basic (s ^ ".imp"))
+ val is = TextIO.openIn (File.platform_path src_location)
val inp = TextIO.inputAll is
val _ = TextIO.closeIn is
val orig_source = Source.of_string inp
@@ -148,7 +149,7 @@
fun apply [] thy = thy
| apply (f::fs) thy = apply fs (f thy)
in
- apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
+ apply (set_replaying_thy s :: Sign.add_path s :: fst (importP token_list))
end
fun create_int_thms thyname thy =
@@ -167,15 +168,15 @@
NONE => error "Import data already cleared - forgotten a setup_theory?"
| SOME _ => ImportData.put NONE thy
-val setup_theory = Parse.name
+val setup_theory = (Parse.name -- Parse.name)
>>
- (fn thyname =>
+ (fn (location, thyname) =>
fn thy =>
(case HOL4DefThy.get thy of
NoImport => thy
| Generating _ => error "Currently generating a theory!"
| Replaying _ => thy |> clear_import_thy)
- |> import_thy thyname
+ |> import_thy location thyname
|> create_int_thms thyname)
fun end_setup toks =