--- a/NEWS Mon Dec 20 15:37:25 2010 +0100
+++ b/NEWS Mon Dec 20 17:31:58 2010 +0100
@@ -603,7 +603,9 @@
*** FOL and ZF ***
-* All constant names are now qualified. INCOMPATIBILITY.
+* All constant names are now qualified internally and use proper
+identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.
+
*** ML ***
--- a/src/CTT/CTT.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/CTT/CTT.thy Mon Dec 20 17:31:58 2010 +0100
@@ -54,7 +54,7 @@
lambda :: "(i => i) => i" (binder "lam " 10)
app :: "[i,i]=>i" (infixl "`" 60)
(*Natural numbers*)
- "0" :: "i" ("0")
+ Zero :: "i" ("0")
(*Pairing*)
pair :: "[i,i]=>i" ("(1<_,/_>)")
--- a/src/FOL/FOL.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/FOL.thy Mon Dec 20 17:31:58 2010 +0100
@@ -175,7 +175,7 @@
(
val thy = @{theory}
type claset = Cla.claset
- val equality_name = @{const_name "op ="}
+ val equality_name = @{const_name eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
val ccontr = @{thm ccontr}
@@ -391,4 +391,7 @@
setup Induct.setup
declare case_split [cases type: o]
+
+hide_const (open) eq
+
end
--- a/src/FOL/IFOL.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/IFOL.thy Mon Dec 20 17:31:58 2010 +0100
@@ -42,13 +42,13 @@
(* Connectives *)
- "op =" :: "['a, 'a] => o" (infixl "=" 50)
+ eq :: "['a, 'a] => o" (infixl "=" 50)
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o, o] => o" (infixr "&" 35)
- "op |" :: "[o, o] => o" (infixr "|" 30)
- "op -->" :: "[o, o] => o" (infixr "-->" 25)
- "op <->" :: "[o, o] => o" (infixr "<->" 25)
+ conj :: "[o, o] => o" (infixr "&" 35)
+ disj :: "[o, o] => o" (infixr "|" 30)
+ imp :: "[o, o] => o" (infixr "-->" 25)
+ iff :: "[o, o] => o" (infixr "<->" 25)
(* Quantifiers *)
@@ -69,28 +69,24 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10) and
- "op -->" (infixr "\<longrightarrow>" 25) and
- "op <->" (infixr "\<longleftrightarrow>" 25)
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
finalconsts
- False All Ex
- "op ="
- "op &"
- "op |"
- "op -->"
+ False All Ex eq conj disj imp
axioms
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Dec 20 17:31:58 2010 +0100
@@ -156,7 +156,7 @@
end;
*}
-local_setup {* Config.put show_hyps true *}
+declare [[show_hyps]]
ML {*
check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
--- a/src/FOL/ex/Nat.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/Nat.thy Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOL/ex/ROOT.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/ex/ROOT.ML Mon Dec 20 17:31:58 2010 +0100
@@ -1,8 +1,3 @@
-(* Title: FOL/ex/ROOT.ML
-
-Examples for First-Order Logic.
-*)
-
use_thys [
"First_Order_Logic",
"Natural_Numbers",
@@ -21,5 +16,4 @@
"If"
];
-(*regression test for locales -- sets several global flags!*)
no_document use_thy "Locale_Test/Locale_Test";
--- a/src/FOL/fologic.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/fologic.ML Mon Dec 20 17:31:58 2010 +0100
@@ -50,29 +50,29 @@
(* Logical constants *)
val not = Const (@{const_name Not}, oT --> oT);
-val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
-val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
-val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
-val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
+val conj = Const(@{const_name conj}, [oT,oT]--->oT);
+val disj = Const(@{const_name disj}, [oT,oT]--->oT);
+val imp = Const(@{const_name imp}, [oT,oT]--->oT)
+val iff = Const(@{const_name iff}, [oT,oT]--->oT);
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_iff (t1, t2) = iff $ t1 $ t2;
-fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);
-fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
+fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
--- a/src/FOL/simpdata.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOL/simpdata.ML Mon Dec 20 17:31:58 2010 +0100
@@ -8,15 +8,15 @@
(*Make meta-equalities. The operator below is Trueprop*)
fun mk_meta_eq th = case concl_of th of
- _ $ (Const(@{const_name "op ="},_)$_$_) => th RS @{thm eq_reflection}
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
+ _ $ (Const(@{const_name eq},_)$_$_) => th RS @{thm eq_reflection}
+ | _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| _ =>
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | _ $ (Const(@{const_name "op ="},_)$_$_) => mk_meta_eq th
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T};
@@ -32,7 +32,7 @@
error("Premises and conclusion of congruence rules must use =-equality or <->");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
fun mk_atomize pairs =
@@ -55,11 +55,11 @@
structure Quantifier1 = Quantifier1Fun(
struct
(*abstract syntax*)
- fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
| dest_eq _ = NONE;
- fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_conj((c as Const(@{const_name conj},_)) $ s $ t) = SOME(c,s,t)
| dest_conj _ = NONE;
- fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_imp((c as Const(@{const_name imp},_)) $ s $ t) = SOME(c,s,t)
| dest_imp _ = NONE;
val conj = FOLogic.conj
val imp = FOLogic.imp
--- a/src/FOLP/IFOLP.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/IFOLP.thy Mon Dec 20 17:31:58 2010 +0100
@@ -24,14 +24,14 @@
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
(*** Logical Connectives -- Type Formers ***)
- "op =" :: "['a,'a] => o" (infixl "=" 50)
+ eq :: "['a,'a] => o" (infixl "=" 50)
True :: "o"
False :: "o"
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o,o] => o" (infixr "&" 35)
- "op |" :: "[o,o] => o" (infixr "|" 30)
- "op -->" :: "[o,o] => o" (infixr "-->" 25)
- "op <->" :: "[o,o] => o" (infixr "<->" 25)
+ conj :: "[o,o] => o" (infixr "&" 35)
+ disj :: "[o,o] => o" (infixr "|" 30)
+ imp :: "[o,o] => o" (infixr "-->" 25)
+ iff :: "[o,o] => o" (infixr "<->" 25)
(*Quantifiers*)
All :: "('a => o) => o" (binder "ALL " 10)
Ex :: "('a => o) => o" (binder "EX " 10)
@@ -51,9 +51,9 @@
inr :: "p=>p"
when :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
- "op `" :: "[p,p]=>p" (infixl "`" 60)
+ App :: "[p,p]=>p" (infixl "`" 60)
alll :: "['a=>p]=>p" (binder "all " 55)
- "op ^" :: "[p,'a]=>p" (infixl "^" 55)
+ app :: "[p,'a]=>p" (infixl "^" 55)
exists :: "['a,p]=>p" ("(1[_,/_])")
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
@@ -595,7 +595,7 @@
struct
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const (@{const_name Proof}, _) $
- (Const (@{const_name "op ="}, _) $ t $ u) $ _) = (t, u);
+ (Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u);
val imp_intr = @{thm impI}
--- a/src/FOLP/ex/Nat.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/ex/Nat.thy Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOLP/simpdata.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/FOLP/simpdata.ML Mon Dec 20 17:31:58 2010 +0100
@@ -17,15 +17,15 @@
(* Conversion into rewrite rules *)
fun mk_eq th = case concl_of th of
- _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+ _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name "All"}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, [])];
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 17:31:58 2010 +0100
@@ -13,7 +13,7 @@
consts
- "{|}" :: "'a multiset" ("{|}")
+ emptym :: "'a multiset" ("{|}")
addm :: "['a multiset, 'a] => 'a multiset"
delm :: "['a multiset, 'a] => 'a multiset"
countm :: "['a multiset, 'a => bool] => nat"
--- a/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SUM_OF_SQUARES="$COMPONENT"
--- a/src/HOL/Mirabelle/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mirabelle/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
MIRABELLE_HOME="$COMPONENT"
MIRABELLE_LOGIC=HOL
@@ -5,4 +7,4 @@
MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
MIRABELLE_TIMEOUT=30
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mutabelle/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,7 +1,9 @@
+# -*- shell-script -*- :mode=shellscript:
+
MUTABELLE_HOME="$COMPONENT"
DEFAULT_MUTABELLE_LOGIC=HOL
DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main
DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Mon Dec 20 17:31:58 2010 +0100
@@ -2,7 +2,7 @@
#
# Author: Lukas Bulwahn
#
-# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
+# DESCRIPTION: mutant-testing for counterexample generators and automated tools
PRG="$(basename "$0")"
@@ -16,7 +16,8 @@
echo " -T THEORY parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
echo " -O DIR output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)"
echo
- echo " THEORY is the name of the theory of which all theorems should be mutated and tested"
+ echo " THEORY is the name of the theory of which all theorems should be"
+ echo " mutated and tested."
echo
exit 1
}
--- a/src/HOL/Prolog/Test.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Prolog/Test.thy Mon Dec 20 17:31:58 2010 +0100
@@ -37,9 +37,9 @@
sue :: person
ned :: person
- "23" :: nat ("23")
- "24" :: nat ("24")
- "25" :: nat ("25")
+ nat23 :: nat ("23")
+ nat24 :: nat ("24")
+ nat25 :: nat ("25")
age :: "[person, nat] => bool"
--- a/src/HOL/Tools/ATP/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/ATP/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,1 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_ATP="$COMPONENT"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Dec 20 17:31:58 2010 +0100
@@ -857,8 +857,9 @@
val args' = map (rename_vars_term renaming) args
val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
- (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
+ val solution = TimeLimit.timeLimit timeout (fn prog =>
+ Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
+ (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
--- a/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,5 +1,8 @@
# -*- shell-script -*- :mode=shellscript:
+# FIXME contrib_devel not official
+# FIXME $(type -p swipl) etc. does not allow spaces in file name
+
EXEC_SWIPL="$(choosefrom \
"$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \
"$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Mon Dec 20 17:31:58 2010 +0100
@@ -7,6 +7,9 @@
if [ "$EXEC_SWIPL" = "" ]; then
echo ""
else
+ # FIXME does not allow spaces in $EXEC_SWIPL
+ # FIXME "expr match" not portable
+ # FIXME prefer $(...) in bash
VERSION=`$EXEC_SWIPL --version`
echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'`
fi
--- a/src/HOL/Tools/SMT/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/HOL/Tools/SMT/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
ISABELLE_SMT="$COMPONENT"
REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
--- a/src/LCF/LCF.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/LCF/LCF.thy Mon Dec 20 17:31:58 2010 +0100
@@ -18,13 +18,13 @@
typedecl tr
typedecl void
-typedecl ('a,'b) "*" (infixl "*" 6)
-typedecl ('a,'b) "+" (infixl "+" 5)
+typedecl ('a,'b) prod (infixl "*" 6)
+typedecl ('a,'b) sum (infixl "+" 5)
arities
"fun" :: (cpo, cpo) cpo
- "*" :: (cpo, cpo) cpo
- "+" :: (cpo, cpo) cpo
+ prod :: (cpo, cpo) cpo
+ sum :: (cpo, cpo) cpo
tr :: cpo
void :: cpo
--- a/src/Pure/System/isabelle_system.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Pure/System/isabelle_system.ML Mon Dec 20 17:31:58 2010 +0100
@@ -7,10 +7,11 @@
signature ISABELLE_SYSTEM =
sig
val isabelle_tool: string -> string -> int
- val rm_tree: Path.T -> unit
val mkdirs: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
+ val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+ val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
end;
structure Isabelle_System: ISABELLE_SYSTEM =
@@ -37,8 +38,6 @@
(* directory operations *)
-fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
-
fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
fun mkdir path =
@@ -48,5 +47,33 @@
if File.eq (src, dst) then ()
else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
+
+(* unique tmp files *)
+
+local
+
+fun fresh_path name =
+ let
+ val path = File.tmp_path (Path.basic (name ^ serial_string ()));
+ val _ = File.exists path andalso
+ raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
+ in path end;
+
+fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
+
+in
+
+fun with_tmp_file name f =
+ let val path = fresh_path name
+ in Exn.release (Exn.capture f path before try File.rm path) end;
+
+fun with_tmp_dir name f =
+ let
+ val path = fresh_path name;
+ val _ = mkdirs path;
+ in Exn.release (Exn.capture f path before try rm_tree path) end;
+
end;
+end;
+
--- a/src/Sequents/LK/Nat.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Sequents/LK/Nat.thy Mon Dec 20 17:31:58 2010 +0100
@@ -11,7 +11,7 @@
typedecl nat
arities nat :: "term"
-consts "0" :: nat ("0")
+consts Zero :: nat ("0")
Suc :: "nat=>nat"
rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/Tools/Code/code_target.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/Code/code_target.ML Mon Dec 20 17:31:58 2010 +0100
@@ -397,7 +397,7 @@
then if strict
then error (env_var ^ " not set; cannot check code for " ^ target)
else warning (env_var ^ " not set; skipped checking code for " ^ target)
- else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
+ else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
end;
end; (* local *)
--- a/src/Tools/WWW_Find/etc/settings Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/WWW_Find/etc/settings Mon Dec 20 17:31:58 2010 +0100
@@ -1,7 +1,8 @@
-# the path to lighttpd
+# -*- shell-script -*- :mode=shellscript:
+
LIGHTTPD="/usr/sbin/lighttpd"
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
-
WWWFINDDIR="$COMPONENT"
WWWCONFIG="$WWWFINDDIR/lighttpd.conf"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$WWWFINDDIR/lib/Tools"
--- a/src/Tools/cache_io.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/Tools/cache_io.ML Mon Dec 20 17:31:58 2010 +0100
@@ -7,8 +7,6 @@
signature CACHE_IO =
sig
(*IO wrapper*)
- val with_tmp_file: string -> (Path.T -> 'a) -> 'a
- val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
type result = {
output: string list,
redirected_output: string list,
@@ -34,21 +32,6 @@
val cache_io_prefix = "cache-io-"
-fun with_tmp_file name f =
- let
- val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val x = Exn.capture f path
- val _ = try File.rm path
- in Exn.release x end
-
-fun with_tmp_dir name f =
- let
- val path = File.tmp_path (Path.explode (name ^ serial_string ()))
- val _ = Isabelle_System.mkdirs path
- val x = Exn.capture f path
- val _ = try Isabelle_System.rm_tree path
- in Exn.release x end
-
type result = {
output: string list,
redirected_output: string list,
@@ -62,8 +45,9 @@
in {output=split_lines out2, redirected_output=out1, return_code=rc} end
fun run make_cmd str =
- with_tmp_file cache_io_prefix (fn in_path =>
- with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
+ Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
+ Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
+ raw_run make_cmd str in_path out_path))
(* cache *)
--- a/src/ZF/Tools/datatype_package.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Dec 20 17:31:58 2010 +0100
@@ -91,7 +91,7 @@
(** Define the constructors **)
(*The empty tuple is 0*)
- fun mk_tuple [] = @{const "0"}
+ fun mk_tuple [] = @{const zero}
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
fun mk_inject n k u = Balanced_Tree.access
--- a/src/ZF/Tools/induct_tacs.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Dec 20 17:31:58 2010 +0100
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 17:31:58 2010 +0100
@@ -19,12 +19,12 @@
(* bits *)
-fun mk_bit 0 = Syntax.const @{const_syntax "0"}
- | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
+fun mk_bit 0 = Syntax.const @{const_syntax zero}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax zero}
| mk_bit _ = raise Fail "mk_bit";
-fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
- | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
| dest_bit _ = raise Match;
--- a/src/ZF/Tools/primrec_package.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Dec 20 17:31:58 2010 +0100
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const (@{const_name 0}, Ind_Syntax.iT),
- #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
+ (Const (@{const_name zero}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/ZF.thy Mon Dec 20 17:31:58 2010 +0100
@@ -17,7 +17,7 @@
consts
- "0" :: "i" ("0") --{*the empty set*}
+ zero :: "i" ("0") --{*the empty set*}
Pow :: "i => i" --{*power sets*}
Inf :: "i" --{*infinite set*}
--- a/src/ZF/arith_data.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/arith_data.ML Mon Dec 20 17:31:58 2010 +0100
@@ -24,7 +24,7 @@
val iT = Ind_Syntax.iT;
-val zero = Const(@{const_name 0}, iT);
+val zero = Const(@{const_name zero}, iT);
val succ = Const(@{const_name succ}, iT --> iT);
fun mk_succ t = succ $ t;
val one = mk_succ zero;
@@ -44,7 +44,7 @@
(* dest_sum *)
-fun dest_sum (Const(@{const_name 0},_)) = []
+fun dest_sum (Const(@{const_name zero},_)) = []
| dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
| dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
--- a/src/ZF/ind_syntax.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/ind_syntax.ML Mon Dec 20 17:31:58 2010 +0100
@@ -29,7 +29,7 @@
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
(*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
error"Premises may not be conjuctive"
| chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
@@ -96,7 +96,7 @@
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case filter is_ind (args @ cs) of
- [] => @{const 0}
+ [] => @{const zero}
| u_args => Balanced_Tree.make mk_Un u_args
end;
--- a/src/ZF/simpdata.ML Mon Dec 20 15:37:25 2010 +0100
+++ b/src/ZF/simpdata.ML Mon Dec 20 17:31:58 2010 +0100
@@ -32,8 +32,8 @@
val ZF_conn_pairs =
[(@{const_name Ball}, [@{thm bspec}]),
(@{const_name All}, [@{thm spec}]),
- (@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
+ (@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =