--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/E/eproof Thu Sep 17 19:13:22 2009 +0200
@@ -0,0 +1,92 @@
+#!/usr/bin/perl -w
+#
+# eproof - run E and translate its output into TSTP format
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# This script is a port of a Bash script with the same name coming with
+# E 1.0-004 (written by Stephan Schulz).
+#
+
+
+use File::Basename qw/ dirname /;
+use File::Temp qw/ tempfile /;
+
+
+# E executables
+
+my $edir = dirname($0);
+my $eprover = "$edir/eprover";
+my $epclextract = "$edir/epclextract";
+
+
+# build E command from given commandline arguments
+
+my $format = "";
+my $timelimit = 2000000000; # effectively unlimited
+
+my $eprover_cmd = "'$eprover'";
+foreach (@ARGV) {
+ if (m/--cpu-limit=([0-9]+)/) {
+ $timelimit = $1;
+ }
+
+ if (m/--tstp-out/) {
+ $format = $_;
+ }
+ else {
+ $eprover_cmd = "$eprover_cmd '$_'";
+ }
+}
+$eprover_cmd = "$eprover_cmd -l4 -R -o- --pcl-terms-compressed --pcl-compact";
+
+
+# run E, redirecting output into a temporary file
+
+my ($fh, $filename) = tempfile(UNLINK => 1);
+my $r = system "$eprover_cmd > $filename";
+exit ($r >> 8) if $r != 0;
+
+
+# analyze E output
+
+my @lines = <$fh>;
+my $content = join "", @lines[-60 .. -1];
+ # Note: Like the original eproof, we only look at the last 60 lines.
+
+if ($content =~ m/Total time\s*:\s*([0-9]+\.[0-9]+)/) {
+ $timelimit = $timelimit - $1 - 1;
+
+ if ($content =~ m/No proof found!/) {
+ print "# Problem is satisfiable (or invalid), " .
+ "generating saturation derivation\n";
+ }
+ elsif ($content =~ m/Proof found!/) {
+ print "# Problem is unsatisfiable (or provable), " .
+ "constructing proof object\n";
+ }
+ elsif ($content =~ m/Watchlist is empty!/) {
+ print "# All watchlist clauses generated, constructing derivation\n";
+ }
+ else {
+ print "# Cannot determine problem status\n";
+ exit $r;
+ }
+}
+else {
+ print "# Cannot determine problem status within resource limit\n";
+ exit $r;
+}
+
+
+# translate E output
+
+foreach (@lines) {
+ print if (m/# SZS status/ or m/"# Failure"/);
+}
+$r = system ("exec bash -c \"ulimit -S -t $timelimit; " .
+ "'$epclextract' $format -f --competition-framing $filename\"");
+ # Note: Setting the user time is not supported on Cygwin, i.e., ulimit fails
+ # and prints and error message. How could we then limit the execution time?
+exit ($r >> 8);
+
--- a/NEWS Thu Sep 17 19:13:07 2009 +0200
+++ b/NEWS Thu Sep 17 19:13:22 2009 +0200
@@ -41,14 +41,6 @@
semidefinite programming solvers. For more information and examples
see src/HOL/Library/Sum_Of_Squares.
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.
-INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.
-INCOMPATIBILITY:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
-
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
@@ -57,16 +49,14 @@
* New class "boolean_algebra".
-* Refinements to lattices classes:
- - added boolean_algebra type class
+* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
- renamed ACI to inf_sup_aci
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants renamed:
-
+ corresponding constants (and abbreviations) renamed:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -75,6 +65,14 @@
Set.Union ~> Complete_Lattice.Union
Set.INTER ~> Complete_Lattice.INTER
Set.UNION ~> Complete_Lattice.UNION
+ - more convenient names for set intersection and union:
+ Set.Int ~> Set.inter
+ Set.Un ~> Set.union
+ - mere abbreviations:
+ Set.empty (for bot)
+ Set.UNIV (for top)
+ Complete_Lattice.Inter (for Inf)
+ Complete_Lattice.Union (for Sup)
INCOMPATIBILITY.
@@ -87,7 +85,7 @@
INCOMPATIBILITY.
* Power operations on relations and functions are now one dedicate
-constant compow with infix syntax "^^". Power operations on
+constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
in class power. INCOMPATIBILITY.
@@ -129,6 +127,9 @@
ATPs down considerably but eliminates a source of unsound "proofs"
that fail later.
+* New method metisFT: A version of metis that uses full type information
+in order to avoid failures of proof reconstruction.
+
* Discontinued ancient tradition to suffix certain ML module names
with "_package", e.g.:
--- a/src/HOL/Complete_Lattice.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy Thu Sep 17 19:13:22 2009 +0200
@@ -203,8 +203,8 @@
subsection {* Union *}
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> \<Squnion>S"
notation (xsymbols)
Union ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
- by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+ by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
qed
lemma Union_iff [simp, noatp]:
@@ -314,7 +314,7 @@
lemma UNION_eq_Union_image:
"(\<Union>x\<in>A. B x) = \<Union>(B`A)"
- by (simp add: SUPR_def SUPR_set_eq [symmetric] Sup_set_eq)
+ by (simp add: SUPR_def SUPR_set_eq [symmetric])
lemma Union_def:
"\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
subsection {* Inter *}
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> \<Sqinter>S"
notation (xsymbols)
Inter ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
- by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+ by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -541,7 +541,7 @@
lemma INTER_eq_Inter_image:
"(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (simp add: INFI_def INFI_set_eq [symmetric] Inf_set_eq)
+ by (simp add: INFI_def INFI_set_eq [symmetric])
lemma Inter_def:
"\<Inter>S = (\<Inter>x\<in>S. x)"
--- a/src/HOL/Inductive.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Inductive.thy Thu Sep 17 19:13:22 2009 +0200
@@ -111,8 +111,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms unfolding Sup_set_eq [symmetric]
- by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct [where P=P])
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
--- a/src/HOL/Library/Executable_Set.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy Thu Sep 17 19:13:22 2009 +0200
@@ -8,7 +8,7 @@
imports Main Fset
begin
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
declare member [code]
@@ -24,9 +24,7 @@
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
[code del]: "eq_set = op ="
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
lemma [code]:
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
declare Inter_image_eq [symmetric, code]
declare Union_image_eq [symmetric, code]
-
-subsection {* Rewrites for primitive operations *}
-
declare List_Set.project_def [symmetric, code_unfold]
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter = Complete_Lattice.Inter"
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
ML {*
nonfix inter;
@@ -75,8 +80,8 @@
"op \<union>" ("{*Fset.union*}")
"op \<inter>" ("{*Fset.inter*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
- "Complete_Lattice.Union" ("{*Fset.Union*}")
- "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+ "Union" ("{*Fset.Union*}")
+ "Inter" ("{*Fset.Inter*}")
card ("{*Fset.card*}")
fold ("{*foldl o flip*}")
--- a/src/HOL/Nominal/Examples/Class.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Thu Sep 17 19:13:22 2009 +0200
@@ -11134,7 +11134,6 @@
shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
and "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
--- a/src/HOL/SetInterval.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/SetInterval.thy Thu Sep 17 19:13:22 2009 +0200
@@ -514,6 +514,30 @@
qed
+subsubsection {* Proving Inclusions and Equalities between Unions *}
+
+lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
+ by (auto simp add: atLeast0LessThan)
+
+lemma UN_finite_subset: "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C"
+ by (subst UN_UN_finite_eq [symmetric]) blast
+
+lemma UN_finite2_subset:
+ assumes sb: "!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)"
+ shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
+proof (rule UN_finite_subset)
+ fix n
+ have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n}. B i)" by (rule sb)
+ also have "... \<subseteq> (\<Union>n::nat. \<Union>i\<in>{0..<n}. B i)" by blast
+ also have "... = (\<Union>n. B n)" by (simp add: UN_UN_finite_eq)
+ finally show "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>n. B n)" .
+qed
+
+lemma UN_finite2_eq:
+ "(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)"
+ by (iprover intro: subset_antisym UN_finite2_subset elim: equalityE)
+
+
subsubsection {* Cardinality *}
lemma card_lessThan [simp]: "card {..<u} = u"
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Sep 17 19:13:22 2009 +0200
@@ -79,14 +79,17 @@
preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
(* write out problem file and call prover *)
- val perl_script = "perl -w $ISABELLE_ATP_MANAGER/lib/scripts/local_atp.pl"
- fun cmd_line probfile = perl_script ^ " '" ^ space_implode " "
- [File.shell_path cmd, args, File.platform_path probfile] ^ "'"
+ fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
+ [File.shell_path cmd, args, File.platform_path probfile] ^ " ; } 2>&1"
fun split_time s =
let
val split = String.tokens (fn c => str c = "\n")
val (proof, t) = s |> split |> split_last |> apfst cat_lines
- val time = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
+ fun as_num f = f >> (fst o read_int)
+ val num = as_num (Scan.many1 Symbol.is_ascii_digit)
+ val digit = Scan.one Symbol.is_ascii_digit
+ val num3 = as_num (digit ::: digit ::: (digit >> single))
+ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
in (proof, as_time t) end
fun run_on probfile =
@@ -97,7 +100,7 @@
else error ("Bad executable: " ^ Path.implode cmd)
(* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
- fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
+ fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE
fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
--- a/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl Thu Sep 17 19:13:07 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-use POSIX qw(setsid);
-
-$SIG{'INT'} = "DEFAULT";
-
-defined (my $pid = fork) or die "$!";
-if (not $pid) {
- POSIX::setsid or die $!;
- exec @ARGV;
-}
-else {
- wait;
- my ($user, $system, $cuser, $csystem) = times;
- my $time = ($user + $cuser) * 1000;
- print "$time\n";
-}
--- a/src/HOL/UNITY/Transformers.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy Thu Sep 17 19:13:22 2009 +0200
@@ -88,7 +88,7 @@
done
lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def, blast)
text{*These two theorems justify the claim that @{term wens} returns the
weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Sup_set_eq, blast)
+ ensures_def transient_def, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -120,7 +120,7 @@
text{*Assertion 4.17 in the thesis*}
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
--{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
lemma wens_single_eq:
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOL/ex/CTL.thy Thu Sep 17 19:13:07 2009 +0200
+++ b/src/HOL/ex/CTL.thy Thu Sep 17 19:13:22 2009 +0200
@@ -95,7 +95,7 @@
proof
assume "x \<in> gfp (\<lambda>s. - f (- s))"
then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
- by (auto simp add: gfp_def Sup_set_eq)
+ by (auto simp add: gfp_def)
then have "f (- u) \<subseteq> - u" by auto
then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
from l and this have "x \<notin> u" by auto
--- a/src/Pure/Concurrent/future.ML Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Sep 17 19:13:22 2009 +0200
@@ -84,7 +84,7 @@
fun group_of (Future {group, ...}) = group;
fun result_of (Future {result, ...}) = result;
-fun peek x = Synchronized.peek (result_of x);
+fun peek x = Synchronized.value (result_of x);
fun is_finished x = is_some (peek x);
fun value x = Future
--- a/src/Pure/Concurrent/synchronized.ML Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Thu Sep 17 19:13:22 2009 +0200
@@ -8,7 +8,6 @@
sig
type 'a var
val var: string -> 'a -> 'a var
- val peek: 'a var -> 'a
val value: 'a var -> 'a
val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -33,9 +32,7 @@
cond = ConditionVar.conditionVar (),
var = ref x};
-fun peek (Var {var, ...}) = ! var; (*unsynchronized!*)
-
-fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
+fun value (Var {var, ...}) = ! var;
(* synchronized access *)
--- a/src/Pure/General/binding.ML Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/General/binding.ML Thu Sep 17 19:13:22 2009 +0200
@@ -30,18 +30,19 @@
val str_of: binding -> string
end;
-structure Binding:> BINDING =
+structure Binding: BINDING =
struct
(** representation **)
(* datatype *)
-datatype binding = Binding of
+abstype binding = Binding of
{prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
- pos: Position.T}; (*source position*)
+ pos: Position.T} (*source position*)
+with
fun make_binding (prefix, qualifier, name, pos) =
Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
end;
+end;
type binding = Binding.binding;
--- a/src/Pure/General/linear_set.scala Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/General/linear_set.scala Thu Sep 17 19:13:22 2009 +0200
@@ -93,11 +93,11 @@
}
def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
- (elems :\ this)((elem: A, ls: Linear_Set[A]) => ls.insert_after(hook, elem))
+ (elems :\ this)((elem, set) => set.insert_after(hook, elem))
def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
{
- if (!rep.first.isDefined) this
+ if (isEmpty) this
else {
val next =
if (from == rep.last) None
@@ -123,7 +123,7 @@
def hasNext = next_elem.isDefined
def next = {
val elem = next_elem.get
- next_elem = if (rep.nexts.isDefinedAt(elem)) Some(rep.nexts(elem)) else None
+ next_elem = rep.nexts.get(elem)
elem
}
}
--- a/src/Pure/thm.ML Thu Sep 17 19:13:07 2009 +0200
+++ b/src/Pure/thm.ML Thu Sep 17 19:13:22 2009 +0200
@@ -153,7 +153,7 @@
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
-structure Thm:> THM =
+structure Thm: THM =
struct
structure Pt = Proofterm;
@@ -163,11 +163,12 @@
(** certified types **)
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
{thy_ref: theory_ref,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
fun rep_ctyp (Ctyp args) = args;
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
@@ -189,12 +190,13 @@
(** certified terms **)
(*certified terms with checked typ, maxidx, and sorts*)
-datatype cterm = Cterm of
+abstype cterm = Cterm of
{thy_ref: theory_ref,
t: term,
T: typ,
maxidx: int,
- sorts: sort OrdList.T};
+ sorts: sort OrdList.T}
+with
exception CTERM of string * cterm list;
@@ -337,7 +339,7 @@
(*** Derivations and Theorems ***)
-datatype thm = Thm of
+abstype thm = Thm of
deriv * (*derivation*)
{thy_ref: theory_ref, (*dynamic reference to theory*)
tags: Properties.T, (*additional annotations/comments*)
@@ -348,7 +350,8 @@
prop: term} (*conclusion*)
and deriv = Deriv of
{promises: (serial * thm future) OrdList.T,
- body: Pt.proof_body};
+ body: Pt.proof_body}
+with
type conv = cterm -> thm;
@@ -1718,6 +1721,10 @@
end
end;
+end;
+end;
+end;
+
(* authentic derivation names *)