Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-4096
+4096
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged
2009-06-12, by bulwahn
added lemma
2009-06-11, by bulwahn
added lemma
2009-06-11, by bulwahn
masking proof with a quick-and-dirty step
2009-06-11, by bulwahn
merged
2009-06-11, by bulwahn
improved infrastructure of predicate compiler for adding manual introduction rules
2009-06-11, by bulwahn
merged
2009-06-11, by huffman
move lemma compact_Times; generalize more lemmas
2009-06-11, by huffman
generalize lemma edelstein_fix
2009-06-11, by huffman
generalize lemmas
2009-06-11, by huffman
add lemmas about closed sets
2009-06-11, by huffman
new lemmas
2009-06-11, by huffman
new lemmas
2009-06-11, by huffman
theorem attribute [tendsto_intros]
2009-06-11, by huffman
subsection for real instances; new lemmas for open sets of reals
2009-06-11, by huffman
cleaned up some proofs
2009-06-11, by huffman
new lemmas
2009-06-11, by huffman
rewrite proof of compact_convex_combinations to avoid pastecart and vec1
2009-06-10, by huffman
heine_borel instance for products
2009-06-10, by huffman
use constants subseq, incseq, monoseq
2009-06-10, by huffman
remove uses of vec1 in continuity lemmas
2009-06-09, by huffman
two finiteness lemmas by Robert Himmelmann
2009-06-11, by nipkow
merged, reverting workarounds on both sides;
2009-06-11, by wenzelm
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;
2009-06-11, by wenzelm
added sporadic (Local)Theory.checkpoint, to enable parallel proof checking;
2009-06-11, by wenzelm
merged
2009-06-11, by wenzelm
merged
2009-06-10, by wenzelm
making isatest happy; but misunderstanding remains
2009-06-11, by bulwahn
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
2009-06-10, by bulwahn
tuned; corrected exception handling
2009-06-10, by bulwahn
tuned;
2009-06-10, by wenzelm
discontinued escaped symbols;
2009-06-10, by wenzelm
eliminated escaped symbols;
2009-06-10, by wenzelm
discontinued escaped symbols such as \\<forall> -- only one backslash should be used;
2009-06-10, by wenzelm
updated generated files;
2009-06-10, by wenzelm
allow Isabelle symbols within low-level ML source;
2009-06-10, by wenzelm
reraise exceptions to preserve position information;
2009-06-10, by wenzelm
simplified Graph.extend;
2009-06-10, by wenzelm
removed unused make;
2009-06-10, by wenzelm
merged
2009-06-09, by wenzelm
merged
2009-06-09, by huffman
instance heine_borel < complete_space; generalize many lemmas to class heine_borel
2009-06-09, by huffman
new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^
2009-06-09, by huffman
generalize compact/closure lemmas
2009-06-08, by huffman
add lemma complete_imp_closed
2009-06-08, by huffman
generalize constant 'bounded' to class metric_space
2009-06-08, by huffman
generalize lemmas compact_imp_bounded, compact_imp_closed
2009-06-08, by huffman
generalize more lemmas
2009-06-08, by huffman
generalize constant 'indirection'
2009-06-08, by huffman
lemmas about linear, bilinear
2009-06-08, by huffman
generalize constant 'complete'
2009-06-08, by huffman
generalize lemmas eventually_within_interior, lim_within_interior
2009-06-08, by huffman
generalize more lemmas
2009-06-08, by huffman
generalize some lemmas
2009-06-08, by huffman
avoiding duplicate definitions of executable functions
2009-06-09, by bulwahn
tuned;
2009-06-09, by wenzelm
more native Scala style;
2009-06-09, by wenzelm
tuned;
2009-06-09, by wenzelm
simplified IsabelleSystem.platform_path for cygwin;
2009-06-09, by wenzelm
merged
2009-06-09, by wenzelm
removed duplicate lemmas
2009-06-09, by himmelma
removed general graph functions in the predicate compiler
2009-06-09, by bulwahn
added graph builders
2009-06-09, by bulwahn
removed debug messages
2009-06-09, by bulwahn
refactoring the predicate compiler
2009-06-09, by bulwahn
merged
2009-06-09, by chaieb
Tuned sos tactic to reject non SOS goals
2009-06-09, by chaieb
tuned
2009-06-09, by boehmes
fast_lin_arith uses proper multiplication instead of unfolding to additions
2009-06-08, by boehmes
more lemmas
2009-06-08, by nipkow
Better approximation of cos around pi.
2009-06-08, by hoelzl
merged
2009-06-08, by huffman
merged
2009-06-07, by huffman
new lemma
2009-06-08, by nipkow
merged
2009-06-08, by haftmann
merged
2009-06-08, by haftmann
proper deresolving of class relations and class parameters in SML
2009-06-08, by haftmann
New lemma
2009-06-08, by nipkow
eliminated hardwired Cygwin setup;
2009-06-08, by wenzelm
Accessing the Cygwin installation.
2009-06-08, by wenzelm
static IsabelleSystem.charset;
2009-06-07, by wenzelm
isabelle getenv: option -d;
2009-06-07, by wenzelm
no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;
2009-06-06, by wenzelm
updated version;
2009-06-06, by wenzelm
fix type of open
2009-06-07, by huffman
new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
2009-06-07, by huffman
replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-07, by huffman
generalize tendsto lemmas for products
2009-06-07, by huffman
move definitions of open, closed to RealVector.thy
2009-06-07, by huffman
lemmas islimptI, islimptE; generalize open_inter_closure_subset
2009-06-06, by huffman
generalize tendsto to class topological_space
2009-06-06, by huffman
put syntax for tendsto in Limits.thy; rename variables
2009-06-05, by huffman
constant "chars" of all characters
2009-06-08, by haftmann
added infrastructure for definitorial construction of generators for datatypes
2009-06-08, by haftmann
constant "chars" of all characters
2009-06-08, by haftmann
added generator for char and trivial generator for String.literal
2009-06-08, by haftmann
using constant "chars"
2009-06-08, by haftmann
method linarith
2009-06-08, by haftmann
reraise exceptions to preserve position information;
2009-06-06, by wenzelm
ML_Compiler.exn_message;
2009-06-06, by wenzelm
ML_Compiler.exn_message;
2009-06-06, by wenzelm
added exn_message (formerly in toplevel.ML);
2009-06-06, by wenzelm
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-06, by wenzelm
report_parse_tree: ML_open, ML_struct;
2009-06-06, by wenzelm
export end_pos_of;
2009-06-06, by wenzelm
use: tuned error;
2009-06-06, by wenzelm
added markup ML_open, ML_struct;
2009-06-06, by wenzelm
use_text: pass file name to compiler, tuned;
2009-06-06, by wenzelm
tuned comments;
2009-06-06, by wenzelm
removed obsolete YXML/XML.detect;
2009-06-05, by wenzelm
Approximation: Corrected precision of ln on all real values
2009-06-05, by hoelzl
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
2009-06-04, by hoelzl
CONTRIBUTORS
2009-06-05, by haftmann
merged
2009-06-05, by haftmann
tuned proofs
2009-06-05, by haftmann
added mk_valtermify_app and mk_random
2009-06-05, by haftmann
Set.insert with authentic syntax
2009-06-05, by haftmann
merged
2009-06-05, by haftmann
Set.insert with authentic syntax
2009-06-05, by haftmann
added trees implementing mappings
2009-06-04, by haftmann
avoid Library.foldl_map
2009-06-04, by haftmann
class replaces axclass
2009-06-04, by haftmann
insert now qualified and with authentic syntax
2009-06-04, by haftmann
lemma about List.foldl and Finite_Set.fold
2009-06-04, by haftmann
dropped legacy ML bindings; tuned
2009-06-04, by haftmann
lemmas about basic set operations and Finite_Set.fold
2009-06-04, by haftmann
merged
2009-06-05, by nipkow
new lemma
2009-06-05, by nipkow
merged
2009-06-05, by huffman
fix type of hnorm
2009-06-05, by huffman
define netlimit in terms of eventually
2009-06-04, by huffman
generalize type of 'at' to topological_space; generalize some lemmas
2009-06-04, by huffman
add extra type constraints for dist, norm
2009-06-04, by huffman
generalize norm method to work over class real_normed_vector
2009-06-04, by huffman
example settings for Poly/ML 5.3 (experimental);
2009-06-04, by wenzelm
uniform (short) ids on both sides;
2009-06-04, by wenzelm
merged
2009-06-04, by wenzelm
finite lemmas
2009-06-04, by nipkow
made SML/NJ happy
2009-06-04, by haftmann
merged
2009-06-04, by nipkow
A few finite lemmas
2009-06-04, by nipkow
removed unused location_of;
2009-06-04, by wenzelm
retrieve ML source files;
2009-06-04, by wenzelm
export file_name;
2009-06-04, by wenzelm
more robust treatment of bootstrap source positions;
2009-06-04, by wenzelm
less experimental polyml-5.3;
2009-06-04, by wenzelm
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
2009-06-04, by wenzelm
exn_message/raised: ML_Compiler.exception_position;
2009-06-04, by wenzelm
eliminated costly registration of tokens;
2009-06-04, by wenzelm
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
2009-06-04, by wenzelm
added exception_position (dummy);
2009-06-04, by wenzelm
reraise exceptions to preserve original position (ML system specific);
2009-06-04, by wenzelm
tuned signature;
2009-06-04, by wenzelm
export esc;
2009-06-04, by wenzelm
export value;
2009-06-04, by wenzelm
uniform default settings for E, Vampire, SPASS;
2009-06-04, by wenzelm
merged
2009-06-03, by huffman
add classes for t0, t1, and t2 spaces
2009-06-03, by huffman
generalize type of islimpt
2009-06-03, by huffman
more [code del] declarations
2009-06-03, by huffman
generalize some constants and lemmas to class topological_space
2009-06-03, by huffman
replace class open with class topo
2009-06-03, by huffman
open_dist instance for vectors
2009-06-03, by huffman
instance * :: topological_space
2009-06-03, by huffman
class real_inner derives from open_dist
2009-06-03, by huffman
introduce class topological_space as a superclass of metric_space
2009-06-03, by huffman
Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
2009-06-03, by hoelzl
additional debugging
2009-06-03, by immler
include chain-ths in every prover-call
2009-06-03, by immler
split preparing clauses and writing problemfile;
2009-06-03, by immler
merged
2009-06-03, by huffman
merged
2009-06-02, by huffman
instance ^ :: complete_space
2009-06-02, by huffman
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
2009-06-02, by huffman
generalize type of constant lim
2009-06-02, by huffman
class complete_space
2009-06-02, by huffman
generalize constant uniformly_continuous_on
2009-06-02, by huffman
generalize more constants
2009-06-02, by huffman
generalize type of bounded
2009-06-02, by huffman
generalize lemma norm_pastecart
2009-06-02, by huffman
generalize lemma norm_triangle_sub
2009-06-02, by huffman
generalize lemma Lim_unique
2009-06-02, by huffman
generalize lemma closed_cball
2009-06-02, by huffman
generalize Lim_transform lemmas
2009-06-02, by huffman
generalize lemma interior_closed_Un_empty_interior
2009-06-02, by huffman
reuse definition of nets from Limits.thy
2009-06-02, by huffman
replace filters with filter bases
2009-06-02, by huffman
generalize type of 'at' to metric_space
2009-06-02, by huffman
redefine nets as filter bases
2009-06-02, by huffman
new lemmas
2009-06-02, by huffman
limits of Pair using filters
2009-06-01, by huffman
Removed usage of reference in reification
2009-06-03, by hoelzl
corrected spacing in reflection
2009-06-02, by hoelzl
switch at-sml-dev-e back to full test on macbroy23
2009-06-03, by kleing
IsabelleProcess: emit status "ready" after initialization and reports;
2009-06-02, by wenzelm
moved restrict_map_insert to theory Map
2009-06-02, by haftmann
merged
2009-06-02, by haftmann
added Landau theory
2009-06-02, by haftmann
added/moved lemmas by Andreas Lochbihler
2009-06-02, by haftmann
added Fin_Fun theory
2009-06-02, by haftmann
tuned code generator test theories
2009-06-02, by haftmann
OCaml builtin intergers are elusive; avoid
2009-06-02, by haftmann
more aggresive bracketing of let expressions
2009-06-02, by haftmann
tuned whitespace
2009-06-02, by haftmann
merged
2009-06-02, by wenzelm
merged
2009-06-02, by wenzelm
merged
2009-06-02, by chaieb
merged
2009-06-02, by chaieb
merged
2009-06-02, by chaieb
Reverses idempotent; radical of E; generalized logarithm;
2009-06-01, by chaieb
made SML/NJ happy;
2009-06-02, by wenzelm
merged
2009-06-02, by wenzelm
use algebra_simps instead of ring_simps
2009-06-02, by hoelzl
merged, resolving conflict in src/Pure/Isar/attrib.ML;
2009-06-02, by wenzelm
Generalized Integral_add
2009-06-02, by hoelzl
Added theorems about distinct & concat, map & replicate and concat & replicate
2009-06-02, by hoelzl
merged
2009-06-02, by berghofe
Fixed broken code dealing with alternative names.
2009-06-02, by berghofe
Enclosed parts of subsection in @{text ...} to make LaTeX happy.
2009-06-02, by berghofe
Added Convex_Euclidean_Space.thy again.
2009-06-02, by berghofe
made SML/NJ happy
2009-06-02, by haftmann
declare Bfun_def [code del]
2009-06-01, by huffman
simp del -> code del
2009-06-01, by huffman
limits of inverse using filters
2009-06-01, by huffman
merged
2009-06-01, by huffman
add [code del] declarations
2009-06-01, by huffman
add dependency on Limits.thy
2009-06-01, by huffman
new lemma
2009-06-01, by nipkow
merged
2009-05-31, by huffman
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
2009-05-31, by huffman
more abstract properties of eventually
2009-05-31, by huffman
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
2009-05-31, by huffman
generalize at function to class perfect_space
2009-05-29, by huffman
generalize topological notions to class metric_space; add class perfect_space
2009-05-29, by huffman
instance ^ :: (metric_space, finite) metric_space
2009-05-29, by huffman
generalize tendsto and related constants to class metric_space
2009-05-29, by huffman
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
2009-05-29, by huffman
remove duplicate cauchy constant
2009-05-29, by huffman
fix reference to LIM_def
2009-05-29, by huffman
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
2009-05-29, by huffman
generalize constants from Lim.thy to class metric_space
2009-05-29, by huffman
LIMSEQ_def -> LIMSEQ_iff
2009-05-28, by huffman
generalize constants in SEQ.thy to class metric_space
2009-05-28, by huffman
early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
2009-06-02, by wenzelm
structure ML_Compiler;
2009-06-01, by wenzelm
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
2009-06-01, by wenzelm
added flatten;
2009-06-01, by wenzelm
tuned signature;
2009-06-01, by wenzelm
export secure_mltext;
2009-06-01, by wenzelm
tuned comments;
2009-06-01, by wenzelm
maintain tokens within common ML environment;
2009-06-01, by wenzelm
ML_Env;
2009-06-01, by wenzelm
slightly later setup of ML and secure operations;
2009-06-01, by wenzelm
moved local ML environment to separate module ML_Env;
2009-06-01, by wenzelm
removed print function from global ML name space, to reduce risk of surprises;
2009-06-01, by wenzelm
made SML/NJ happy;
2009-06-01, by wenzelm
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
2009-05-31, by wenzelm
eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;
2009-05-31, by wenzelm
provide local dummy version of makestring -- NB: makestring is fragile and not portable, it should not occur in repository sources;
2009-05-31, by wenzelm
no longer open PolyML -- to avoid surprises within the global name space;
2009-05-31, by wenzelm
explicit PolyML qualification;
2009-05-31, by wenzelm
removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
2009-05-31, by wenzelm
test experimental Poly/ML 5.3;
2009-05-31, by wenzelm
removed obsolete COPYDB flag;
2009-05-31, by wenzelm
explicit PolyML.install_pp;
2009-05-31, by wenzelm
renamed polyml_pp.ML to pp_polyml.ML;
2009-05-31, by wenzelm
more modular setup of runtime compilation;
2009-05-31, by wenzelm
more precise version information;
2009-05-31, by wenzelm
uniform treatment of shellscript mode;
2009-05-31, by wenzelm
updated example settings;
2009-05-31, by wenzelm
discontinued support for Poly/ML 4.x versions;
2009-05-31, by wenzelm
ISABELLE_USEDIR_OPTIONS: proper word splitting of quoted options (via array variable and special expansion, cf. "$@");
2009-05-30, by wenzelm
eliminated old Attrib.add_attributes (and Attrib.syntax);
2009-05-30, by wenzelm
modernized attribute setup;
2009-05-30, by wenzelm
eliminated old Method.add_method(s);
2009-05-30, by wenzelm
removed obsolete combinators for method args;
2009-05-30, by wenzelm
proper signature constraint;
2009-05-30, by wenzelm
minimal signature cleanup;
2009-05-30, by wenzelm
modernized method setup;
2009-05-30, by wenzelm
modernized method setup;
2009-05-30, by wenzelm
tuned;
2009-05-30, by wenzelm
tuned;
2009-05-30, by wenzelm
simps with mandatory name prefix
2009-05-30, by haftmann
corrected bound/unbounded flag for nat numerals
2009-05-30, by haftmann
removed dead theory Relation_Power
2009-05-29, by haftmann
fix reference to dist_def
2009-05-28, by huffman
definition of dist for complex
2009-05-28, by huffman
fix references to dist_def
2009-05-28, by huffman
define dist for products
2009-05-28, by huffman
move dist operation to new metric_space class
2009-05-28, by huffman
remove hard tabs, fix indentation
2009-05-28, by huffman
use class field_char_0
2009-05-28, by huffman
merged
2009-05-28, by huffman
generalize dist function to class real_normed_vector
2009-05-28, by huffman
added remark to code
2009-05-28, by bulwahn
Removed Convex_Euclidean_Space.thy from Library.
2009-05-28, by himmelma
Moved some lemmas about intervals to Topology
2009-05-28, by himmelma
Corrected definition of is_interval
2009-05-28, by himmelma
corrected problem in Determinants
2009-05-28, by himmelma
Corrected error in Convex_Euclidean_Space
2009-05-28, by himmelma
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
2009-05-28, by himmelma
merged
2009-05-28, by himmelma
Added Convex_Euclidean_Space.thy
2009-05-28, by himmelma
Changed prioriy of vector_scalar_mult
2009-05-28, by himmelma
addition formulas for fps_sin, fps_cos
2009-05-28, by huffman
use class field_char_0 for fps definitions
2009-05-28, by huffman
merged
2009-05-27, by huffman
add constants sin_coeff, cos_coeff
2009-05-27, by huffman
merged
2009-05-27, by wenzelm
tuned signature of add_primrec_simple
2009-05-27, by haftmann
added lemma select_weight_cons_zero
2009-05-27, by haftmann
added lemma beyond_zero; hide constants
2009-05-27, by haftmann
added lemma about 0 - 1
2009-05-27, by haftmann
merged
2009-05-27, by wenzelm
more lemmas
2009-05-27, by nipkow
merged
2009-05-27, by haftmann
add_primrec_simple
2009-05-26, by haftmann
dropped superfluos prefixes
2009-05-26, by haftmann
separate module for quickcheck generators
2009-05-26, by haftmann
encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
2009-05-26, by huffman
listsum lemmas
2009-05-26, by huffman
clean up some rsum proofs
2009-05-26, by huffman
weakend references to old axclass
2009-05-26, by haftmann
clarified benefit of interpretation
2009-05-26, by haftmann
documented print_codeproc command
2009-05-26, by haftmann
use interval sets with gauge predicate
2009-05-25, by huffman
clean up some proofs
2009-05-25, by huffman
tuned whitespace
2009-05-24, by haftmann
funpow_yield; tuned
2009-05-24, by haftmann
tuned class user space type system code
2009-05-24, by haftmann
dropped Id
2009-05-24, by haftmann
refined construction_interpretation
2009-05-24, by haftmann
exported find_shorzes_path
2009-05-24, by haftmann
merged
2009-05-24, by haftmann
fixed superficial ML lapses introduced in b3c7044d47b6;
2009-05-27, by wenzelm
simplified method syntax;
2009-05-25, by wenzelm
modernized method setup;
2009-05-25, by wenzelm
modernized method setup;
2009-05-25, by wenzelm
proper signature constraints;
2009-05-25, by wenzelm
adapted to Poly/ML SVN 744;
2009-05-25, by wenzelm
removed some obsolete combinators for method args;
2009-05-23, by wenzelm
proper indentation;
2009-05-23, by wenzelm
proper signature constraint;
2009-05-23, by wenzelm
adapted to Poly/ML SVN 719;
2009-05-23, by wenzelm
getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
2009-05-23, by wenzelm
merged
2009-05-22, by huffman
define copy functions using combinators; add checking for failed proofs of induction rules
2009-05-22, by huffman
export ID, oo; add more dtyp operations
2009-05-22, by huffman
add combinators for building copy functions
2009-05-22, by huffman
change representation of Domain_Library.arg
2009-05-21, by huffman
make type Domain_Library.arg abstract
2009-05-21, by huffman
indentation; export Domain_Axioms.calc_axioms
2009-05-20, by huffman
indentation; export Domain_Syntax.calc_syntax
2009-05-20, by huffman
using precompiled Predicate.map
2009-05-21, by haftmann
merged
2009-05-21, by haftmann
re-added corrected version of type copy quickcheck generator
2009-05-21, by haftmann
added Predicate.map in SML environment
2009-05-21, by haftmann
merged
2009-05-21, by webertj
implementation of definitional CNF improved
2009-05-21, by webertj
write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first
2009-05-21, by webertj
fixed typo
2009-05-20, by haftmann
experimental values command
2009-05-20, by haftmann
added Predicate.map
2009-05-20, by haftmann
merged
2009-05-20, by haftmann
tuned
2009-05-20, by haftmann
adjusted to changes in Quickcheck.thy
2009-05-20, by haftmann
eliminated case input syntax on bits
2009-05-20, by haftmann
removed quickcheck generator for type copies temporarily
2009-05-20, by haftmann
avoid potential problem with stale theory
2009-05-20, by haftmann
dropped parentheses
2009-05-20, by haftmann
parse translations for cases are conservative wrt. overloaded constructors
2009-05-20, by haftmann
added generator for type copies (records)
2009-05-20, by haftmann
adjusted to changed theory name
2009-05-20, by haftmann
String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19, by haftmann
moved Code_Index, Random and Quickcheck before Main
2009-05-19, by haftmann
moved Code_Index, Random and Quickcheck before Main
2009-05-19, by haftmann
pretty printing of functional combinators for evaluation code
2009-05-19, by haftmann
new lemma
2009-05-19, by nipkow
merged
2009-05-18, by chaieb
FPS composition distributes over inverses, division and arbitrary nth roots. General geometric series theorem
2009-05-18, by chaieb
merged
2009-05-18, by nipkow
fine-tuned elimination of comprehensions involving x=t.
2009-05-18, by nipkow
hide fact log_def -- should not shadow regular log definition
2009-05-18, by haftmann
added example on ML level
2009-05-18, by haftmann
added quickcheck support for numeric types
2009-05-18, by haftmann
generalized lemma map_of_zip_map
2009-05-18, by haftmann
added Code_Index.int_of operation
2009-05-18, by haftmann
tuned term input syntax
2009-05-18, by haftmann
merged
2009-05-18, by haftmann
merged
2009-05-18, by haftmann
merged
2009-05-16, by haftmann
merged
2009-05-16, by haftmann
experimental move of Quickcheck and related theories to HOL image
2009-05-16, by haftmann
experimental addition of quickcheck
2009-05-15, by haftmann
adjusted to changes in theory Quickcheck
2009-05-15, by haftmann
combinators for single-threaded operations
2009-05-15, by haftmann
tuned code postprocessor
2009-05-15, by haftmann
dropped theory Term_Of_Syntax
2009-05-15, by haftmann
hide names in theory Random
2009-05-15, by haftmann
experimental addition of quickcheck
2009-05-15, by haftmann
syntax support for term expressions
2009-05-15, by haftmann
introduced Thm.generatedK
2009-05-18, by haftmann
is a definition
2009-05-17, by haftmann
merged
2009-05-16, by bulwahn
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
2009-05-16, by bulwahn
merged
2009-05-16, by bulwahn
added collection of simplification rules of recursive functions for quickcheck
2009-05-16, by bulwahn
merged
2009-05-16, by bulwahn
added predicate transformation function for code generation
2009-05-15, by bulwahn
added predicate transformation function for code generation
2009-05-15, by bulwahn
proof tuned
2009-05-16, by nipkow
merged
2009-05-16, by nipkow
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
2009-05-16, by nipkow
merged
2009-05-15, by huffman
continuity proofs for approx function on deflations; lemma cast_below_imp_below
2009-05-15, by huffman
allow lazy domain arguments to have class cpo
2009-05-12, by huffman
add cpo_type function
2009-05-12, by huffman
fix domain package parsing of lhs sort constraints
2009-05-12, by huffman
export quiet_mode and trace_domain refs for domain package
2009-05-12, by huffman
new lemma
2009-05-15, by nipkow
merged
2009-05-14, by haftmann
merged
2009-05-14, by haftmann
merged module code_unit.ML into code.ML
2009-05-14, by haftmann
monomorphic code generation for power operations
2009-05-14, by haftmann
preprocessing must consider eq
2009-05-14, by haftmann
quickcheck size starts with 0
2009-05-14, by haftmann
strip sorts while checking pattern subsumption
2009-05-14, by haftmann
rewrite op = == eq handled by simproc
2009-05-14, by haftmann
updated generated document
2009-05-14, by haftmann
merged
2009-05-14, by nipkow
Cleaned up Parity a little
2009-05-14, by nipkow
merged
2009-05-14, by berghofe
merged
2009-05-13, by berghofe
Cleaned up code of function test_term.
2009-05-13, by berghofe
dropped accidental debug messages
2009-05-14, by haftmann
adapted code tutorial to recent changes in code
2009-05-14, by haftmann
more permissive wrt. overloaded constants
2009-05-13, by haftmann
merged
2009-05-13, by haftmann
tuned construction of term_of instances
2009-05-13, by haftmann
tuned construction of term_of instances
2009-05-13, by haftmann
dropped legacy operations
2009-05-13, by haftmann
tuned construction of typerep instances
2009-05-13, by haftmann
tuned and generalized construction of code equations for eq; tuned interface
2009-05-13, by haftmann
added abstract operations for typerep/term_of
2009-05-13, by haftmann
tuned and generalized construction of code equations for eq
2009-05-13, by haftmann
dropped sort constraint on predicate equality
2009-05-13, by haftmann
itself is instance of eq
2009-05-13, by haftmann
Now deals with division
2009-05-13, by chaieb
updated keywords
2009-05-12, by haftmann
split Predicate_Compile examples into separate theory
2009-05-12, by haftmann
adapted to changes in module Code
2009-05-12, by haftmann
values is now a keyword
2009-05-12, by haftmann
merged
2009-05-12, by haftmann
transferred code generator preprocessor into separate module
2009-05-12, by haftmann
marginally tuned
2009-05-12, by haftmann
examples using code_pred
2009-05-12, by haftmann
added dummy values keyword
2009-05-12, by haftmann
tuned exception code
2009-05-12, by haftmann
A generic arithmetic prover based on Positivstellensatz certificates --- also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination
2009-05-12, by chaieb
A decision method for universal multivariate real arithmetic with add
2009-05-12, by chaieb
Isolated decision procedure for noms and the general arithmetic solver
2009-05-12, by chaieb
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
2009-05-12, by chaieb
merged
2009-05-11, by huffman
use Pair/fst/snd instead of cpair/cfst/csnd
2009-05-11, by huffman
use Pair/fst/snd instead of cpair/cfst/csnd
2009-05-11, by huffman
move bifinite instance for product type from Cprod.thy to Bifinite.thy
2009-05-11, by huffman
new lemmas
2009-05-11, by huffman
fixed merge accident
2009-05-11, by haftmann
merged
2009-05-11, by haftmann
avoid latex output problem
2009-05-11, by haftmann
merged
2009-05-11, by haftmann
fixed code_pred command
2009-05-11, by bulwahn
Added pred_code command
2009-05-11, by bulwahn
added general preprocessing of equality in predicates for code generation
2009-04-22, by bulwahn
merged
2009-05-11, by haftmann
merged
2009-05-11, by haftmann
mk_number replaces number_of
2009-05-11, by haftmann
qualified names for Lin_Arith tactics and simprocs
2009-05-11, by haftmann
tuned interface of Lin_Arith
2009-05-11, by haftmann
optimized Approximation by precompiling approx_inequality
2009-05-05, by hoelzl
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
2009-04-29, by hoelzl
merged
2009-05-11, by huffman
newline at end of file
2009-05-11, by huffman
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
2009-05-11, by huffman
removed redundant instance declarations inat :: linorder
2009-05-11, by huffman
merged
2009-05-11, by haftmann
proper error handling for malformed code equations
2009-05-11, by haftmann
corrected deletetion of code equations for constructors
2009-05-11, by haftmann
clarified matter of "proper" flag in code equations
2009-05-11, by haftmann
tuned interface of module Code_Unit
2009-05-11, by haftmann
clarified terminilogy concerning nbe equations
2009-05-11, by haftmann
simplified unoverload/overload policy in code generator preprocessor
2009-05-11, by haftmann
Change to lowercase path names as directed by local pagemasters
2009-05-11, by paulson
merged
2009-05-10, by nipkow
fixed HOLCF proofs
2009-05-10, by nipkow
merged
2009-05-09, by haftmann
interface changes in linarith.ML
2009-05-09, by haftmann
merged
2009-05-09, by nipkow
lemmas by Andreas Lochbihler
2009-05-09, by nipkow
merged
2009-05-08, by nipkow
merged
2009-05-08, by nipkow
more lemmas
2009-05-08, by nipkow
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-05-08, by huffman
fixed theorem statement
2009-05-08, by chaieb
merged
2009-05-08, by chaieb
Generalized distributivity theorems of radicals over multiplication, division and inverses
2009-05-08, by chaieb
proper structure name
2009-05-08, by haftmann
localized (complete) partial order classes
2009-05-08, by haftmann
dropped legacy ml theorem binding
2009-05-08, by haftmann
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-08, by haftmann
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
2009-05-08, by haftmann
generalized simproc for mod
2009-05-08, by haftmann
explicit method linarith
2009-05-08, by haftmann
moved int_factor_simprocs.ML to theory Int
2009-05-08, by haftmann
treat frees driectly by the LCF kernel
2009-05-07, by haftmann
dropped explicit suppport for frees in evaluation conversion stack
2009-05-07, by haftmann
no need for explicit delete declaration
2009-05-07, by haftmann
better to have distinguished class for preorders
2009-05-07, by haftmann
added theory for explicit equivalence relation in preorders
2009-05-07, by haftmann
explicit type_name antiquotations
2009-05-07, by haftmann
explicit type arguments in constants
2009-05-07, by haftmann
merged
2009-05-06, by haftmann
robustifed infrastructure for complex term syntax during code generation
2009-05-06, by haftmann
proper structures for list and string code generation stuff
2009-05-06, by haftmann
explicit type arguments in constants
2009-05-06, by haftmann
confine term setup to Eval serialiser
2009-05-06, by haftmann
adaptation replaces adaption
2009-05-06, by haftmann
refined HOL string theories and corresponding ML fragments
2009-05-06, by haftmann
adaptation replaces adaption
2009-05-06, by haftmann
explicit type arguments in constants
2009-05-06, by haftmann
refined HOL string theories and corresponding ML fragments
2009-05-06, by haftmann
tuned description of overloading
2009-05-06, by haftmann
confine term setup to Eval serialiser
2009-05-06, by haftmann
updated generated file
2009-05-06, by haftmann
new lemmas
2009-05-06, by nipkow
merged
2009-05-06, by nipkow
Prototype introiff option for find_theorems.
2009-05-06, by Timothy Bourke
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
2009-05-06, by huffman
compatible with preorder; bot and top instances
2009-05-06, by haftmann
updated generated files etc/isar-keywords.el and lib/jedit/isabelle.xml
2009-05-04, by immler
tuned
2009-05-04, by immler
added Philipp Meyer's implementation of AtpMinimal
2009-05-04, by immler
removed code_name module
2009-05-04, by haftmann
desymbolization with case selection
2009-05-04, by haftmann
dropped duplicate lemma sum_nonneg_eq_zero_iff
2009-05-04, by haftmann
fixed broken link
2009-05-04, by haftmann
tuned header
2009-05-04, by haftmann
class typerep inherits from type
2009-05-04, by haftmann
use simproc_setup command for cont_proc
2009-04-30, by huffman
used named theorems for declaring numeral simps
2009-04-30, by huffman
clean up unsigned numeral proofs
2009-04-30, by huffman
detect error cases in mk_num, dest_num
2009-04-30, by huffman
add semiring_assoc_fold simproc for unsigned numerals
2009-04-29, by huffman
reorient simproc for unsigned numerals
2009-04-29, by huffman
reimplement reorientation simproc using theory data
2009-04-29, by huffman
use opaque ascription for all HOLCF code
2009-04-29, by huffman
added listsum lemmas
2009-04-29, by nipkow
farewell to class recpower
2009-04-29, by haftmann
merged
2009-04-28, by haftmann
power constraint needed, though
2009-04-28, by haftmann
stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy
2009-04-28, by haftmann
stripped class recpower further
2009-04-28, by haftmann
lemma sum_nonneg_eq_zero_iff
2009-04-28, by haftmann
reorganization of power lemmas
2009-04-28, by haftmann
collected square lemmas in Nat_Numeral
2009-04-28, by haftmann
Symbol.name_of and Name.desymbolize
2009-04-28, by haftmann
prevent potential failure
2009-04-28, by haftmann
ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
2009-04-28, by haftmann
local syntax for Ints; ephermal re-globalization
2009-04-28, by haftmann
dropped reference to class recpower and lemma duplicate
2009-04-28, by haftmann
add proper support for bottom-patterns in fixrec package
2009-04-27, by huffman
merged
2009-04-27, by huffman
add module signature to domain_library.ML
2009-04-22, by huffman
add module signature for domain_theorems.ML
2009-04-22, by huffman
declare take_rews as simp rules
2009-04-22, by huffman
explicit is better than implicit
2009-04-27, by haftmann
whitespace tuning
2009-04-27, by haftmann
cleaned up theory power further
2009-04-27, by haftmann
merged
2009-04-27, by haftmann
merged
2009-04-26, by haftmann
merged
2009-04-26, by haftmann
fixed document generation
2009-04-26, by haftmann
cleaned up Power theory
2009-04-26, by haftmann
merged
2009-04-26, by chaieb
merged
2009-04-26, by chaieb
merged
2009-04-24, by chaieb
more general statements
2009-04-24, by chaieb
tuned
2009-04-27, by Christian Urban
reorganised the section about fresh_star and added lemma pt_fresh_star_pi
2009-04-26, by Christian Urban
reverted slip in theory imports
2009-04-26, by haftmann
adjusted to changes in power syntax
2009-04-26, by haftmann
merged
2009-04-26, by Christian Urban
deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
2009-04-26, by Christian Urban
append prefs at end;
2009-04-25, by wenzelm
merged
2009-04-25, by wenzelm
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
2009-04-25, by Christian Urban
use predefined preferences categories;
2009-04-25, by wenzelm
removed obsolete artifacts;
2009-04-25, by wenzelm
misc cleanup of auto_solve and quickcheck:
2009-04-25, by wenzelm
renamed contrib/SystemOnTPTP/remote to lib/script/SystemOnTPTP, thus leaving contrib empty within the official distribution;
2009-04-25, by wenzelm
post Isabelle2009 version;
2009-04-25, by wenzelm
adjusted to change in code_wellsorted.ML
2009-04-25, by haftmann
merged
2009-04-24, by haftmann
some jokes are just too bad to appear in a theory file
2009-04-24, by haftmann
removed confusion around funpow
2009-04-24, by haftmann
observe distinction between Pure/Tools and Tools more closely
2009-04-24, by haftmann
some experiements towards user interface for predicate compiler
2009-04-24, by haftmann
funpow and relpow with shared "^^" syntax
2009-04-24, by haftmann
generic postprocessing scheme for term evaluations
2009-04-24, by haftmann
added helpless comment
2009-04-24, by haftmann
adaptions due to rearrangment of power operation
2009-04-23, by haftmann
stripped $Id$
2009-04-23, by haftmann
avoid local [code]
2009-04-23, by haftmann
dropped duplication
2009-04-22, by haftmann
code_datatype and power
2009-04-22, by haftmann
tuned
2009-04-22, by haftmann
code_datatype antiquotation; tuned
2009-04-22, by haftmann
more localisation
2009-04-22, by haftmann
power operation defined generic
2009-04-22, by haftmann
fixed compilation of predicate types in ML environment
2009-04-22, by haftmann
merged
2009-04-21, by haftmann
merged
2009-04-20, by haftmann
empty page leads to results on duplex printers as expected
2009-04-20, by haftmann
changes in power operations
2009-04-20, by haftmann
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
2009-04-20, by haftmann
yield is now a static ML function
2009-04-20, by haftmann
power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-04-20, by haftmann
formal declaration of undefined parameters after class instantiation
2009-04-17, by haftmann
power operation on relations now with syntax ^^
2009-04-17, by haftmann
separated funpow, relpow from power on monoids
2009-04-17, by haftmann
static compilation of enumeration type
2009-04-17, by haftmann
re-engineering of evaluation conversions
2009-04-17, by haftmann
tuned
2009-04-17, by haftmann
separate channel for Quickcheck evaluations
2009-04-17, by haftmann
merged
2009-04-17, by haftmann
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
2009-04-17, by haftmann
diagnostic commands now in code_thingol; tuned code of funny continuations
2009-04-17, by haftmann
simplified code
2009-04-17, by haftmann
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
2009-04-17, by haftmann
added both cancel_div_mod_procs
2009-04-17, by haftmann
wellsortedness is no issue for a user manual any more
2009-04-16, by haftmann
whitespace tuning
2009-04-16, by haftmann
added simproc
2009-04-16, by haftmann
dropped unnamed infix
2009-04-16, by haftmann
tuned setups of CancelDivMod
2009-04-16, by haftmann
merged
2009-04-16, by haftmann
tuned order of functions
2009-04-16, by haftmann
generalized some simprocs from int to semiring_div
2009-04-16, by haftmann
tightended specification of class semiring_div
2009-04-16, by haftmann
code generator bootstrap theory src/Tools/Code_Generator.thy
2009-04-15, by haftmann
say farewell to code related to old code_funcgr module
2009-04-15, by haftmann
wrecked old code_funcgr module
2009-04-15, by haftmann
index type is a semiring_div
2009-04-15, by haftmann
theory NatBin now named Nat_Numeral
2009-04-15, by haftmann
default instantiation for unit type
2009-04-15, by haftmann
more coherent developement in Divides.thy and IntDiv.thy
2009-04-15, by haftmann
add more examples to Domain_ex.thy
2009-04-21, by huffman
merged
2009-04-21, by huffman
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
2009-04-21, by huffman
make domain package ML interface more consistent with datatype package; use binding instead of bstring
2009-04-21, by huffman
use Sign.add_consts instead of ContConsts.add_consts
2009-04-21, by huffman
merged
2009-04-21, by huffman
allow infix declarations for type constructors defined with domain package
2009-04-20, by huffman
remove obsolete comments
2009-04-20, by huffman
fix too-specific types in lemmas match_{sinl,sinr}_simps
2009-04-20, by huffman
domain package now generates iff rules for definedness of constructors
2009-04-13, by huffman
change definition of match combinators for fixrec package
2009-04-11, by huffman
domain package: simplify internal proofs of con_rews
2009-04-10, by huffman
set up domain package in Domain.thy
2009-04-10, by huffman
tuned proof
2009-04-21, by krauss
replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.
2009-04-21, by krauss
inlined afterqeds to improve clarity; tuned
2009-04-21, by krauss
simplify computation and consistency checks of argument counts in the input
2009-04-21, by krauss
removed obsolete test tags;
2009-04-20, by wenzelm
back to non-release mode;
2009-04-20, by wenzelm
Added tag Isabelle2009 for changeset 5c8618f95d24
2009-04-19, by wenzelm
merged
Isabelle2009
2009-04-16, by wenzelm
give up file type / dropability for now -- does not work reliably;
2009-04-16, by wenzelm
Added tag isa2009-test for changeset d394a17d4fdb
2009-04-16, by wenzelm
external_prover: "exec" the command line, in order to preserve the exact process context of the "system" invocation (this recovers interruptibility of E-1.0, which assumes to be the process group leader);
2009-04-16, by wenzelm
misc tuning for Isabelle2009;
2009-04-15, by wenzelm
tuned;
2009-04-15, by wenzelm
more generic error message, which also covers more fundamental failure;
2009-04-15, by wenzelm
updated for Isabelle2009;
2009-04-15, by wenzelm
tuned;
2009-04-14, by wenzelm
more robust handling of emacs options -- this is not necessarily an Isabelle process environment yet;
2009-04-14, by wenzelm
merged
2009-04-14, by wenzelm
actually invoke ISABELLE_TOOL;
2009-04-14, by wenzelm
added Haskabelle -- in accordance to website/index.html version f397b96e3ad2;
2009-04-14, by wenzelm
ISABELLE_USEDIR_OPTIONS: less ambitious -M1 by default -- multithreading is largely untested on fringe platforms (cygwin, solaris);
2009-04-14, by wenzelm
misc updates for Isabelle2009;
2009-04-14, by wenzelm
Added tag isa2009-test for changeset dda08b76fa99
2009-04-08, by wenzelm
updated official title of contribution by Johannes Hoelzl;
2009-04-08, by wenzelm
misc tuning and updates;
2009-04-07, by wenzelm
updated doc setup;
2009-04-07, by wenzelm
merged
2009-04-07, by wenzelm
moved generated eps/pdf to main directory, for proper display in dvi;
2009-04-07, by wenzelm
updates for E-1.0-004;
2009-04-07, by wenzelm
tuned manual
2009-04-07, by haftmann
merged
2009-04-06, by haftmann
tuned comment
2009-04-06, by haftmann
Added tag isa2009-test for changeset 613c2eb8aef6
2009-04-06, by wenzelm
tuned whitespace
2009-04-06, by haftmann
merged
2009-04-05, by wenzelm
reverted to explicitly check the presence of a refutation
2009-04-04, by immler
tuned white space;
2009-04-05, by wenzelm
merged
2009-04-05, by wenzelm
\nolinkurl for dvi mode recovers hyphenation of URLs -- this already works by default in PDF mode;
2009-04-05, by wenzelm
removed obsolete website directory -- information derived by website/build;
2009-04-05, by wenzelm
More precise treatement of rational constants by the normalizer for fields
2009-04-05, by chaieb
fixed usage of rational constants
2009-04-05, by chaieb
No Complex_Main needed
2009-04-05, by chaieb
now deals with devision in fields
2009-04-05, by chaieb
fixed formal markup;
2009-04-03, by wenzelm
merged
2009-04-03, by nipkow
Finite_Set: lemma
2009-04-03, by nipkow
single-threaded build;
2009-04-03, by wenzelm
merged
2009-04-03, by berghofe
Added check whether argument types of inductive set agree with types of declared
2009-04-03, by berghofe
added setsum_eq_1_iff
2009-04-03, by nipkow
simplified website/config;
2009-04-02, by wenzelm
Updated to corrected E output messages
2009-04-02, by nipkow
updated keywords (with polyml-experimental);
2009-04-02, by wenzelm
some more HOL-Nominal news;
2009-04-02, by wenzelm
merged
2009-04-02, by wenzelm
tuned signature;
2009-04-02, by wenzelm
misc tuning for release;
2009-04-02, by wenzelm
merged
2009-04-02, by berghofe
Fixed bug in transformation of congruence rule for ==
2009-04-02, by berghofe
some HOL-Nominal news;
2009-04-02, by wenzelm
updates for Isabelle2009 release;
2009-04-02, by wenzelm
tuned;
2009-04-02, by wenzelm
merged
2009-04-02, by wenzelm
misc cleanup and rearrangements for Isabelle2009 release;
2009-04-02, by wenzelm
merged
2009-04-01, by nipkow
cleaned up setprod_zero-related lemmas
2009-04-01, by nipkow
merged
2009-04-01, by huffman
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
2009-04-01, by huffman
added nat_div_gt_0 [simp]
2009-04-01, by nipkow
added setsum_pos_nat
2009-04-01, by nipkow
merged
2009-04-01, by nipkow
added strong_setprod_cong[cong] (in analogy with setsum)
2009-04-01, by nipkow
proper external tikz pictures
2009-04-01, by haftmann
merged
2009-04-01, by wenzelm
tuned comments;
2009-04-01, by wenzelm
merged
2009-04-01, by wenzelm
explicitly check that at least one argument is present to avoid low-level exception
2009-04-01, by krauss
merged
2009-04-01, by wenzelm
included managing_thread in state of AtpManager:
2009-03-31, by immler
domain package registers induction rules
2009-03-31, by huffman
merged
2009-03-31, by wenzelm
Merged.
2009-03-31, by ballarin
Improvements to the text.
2009-03-31, by ballarin
fixed header;
2009-03-31, by wenzelm
fixed header;
2009-03-31, by wenzelm
added dest_conjunctions (cf. Logic.dest_conjunctions);
2009-03-31, by wenzelm
superficial tuning;
2009-03-31, by wenzelm
merged
2009-03-31, by wenzelm
merged
2009-03-31, by wenzelm
schedule_futures: join tasks in regular bottom-up order, which potentially improves resource usage;
2009-03-31, by wenzelm
updated latex requirement;
2009-03-31, by wenzelm
tuned document;
2009-03-31, by wenzelm
replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp);
2009-03-31, by wenzelm
tuned error message;
2009-03-31, by wenzelm
tuned;
2009-03-31, by wenzelm
suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;
2009-03-31, by wenzelm
generalized pull to anamorph
2009-03-31, by haftmann
merged
2009-03-31, by haftmann
ML snippets for experimental evaluation
2009-03-31, by haftmann
merged
2009-03-30, by wenzelm
merged
2009-03-30, by huffman
domain package declares more simp rules
2009-03-30, by huffman
simplified 'print_orders' command;
2009-03-30, by wenzelm
tuned;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
simplify theorem references
2009-03-30, by huffman
added Toplevel.previous_node_of;
2009-03-30, by wenzelm
tuned spacing and formatting;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
terminate watching thread
2009-03-30, by immler
merged
2009-03-30, by wenzelm
no longer delay loading of assoc_fold.ML
2009-03-30, by huffman
qualified_name_of: observe empty case;
2009-03-30, by wenzelm
merged
2009-03-30, by wenzelm
merged
2009-03-30, by huffman
add more lemmas for signed comparisons
2009-03-27, by huffman
use standard parsers provided by SpecParse
2009-03-30, by krauss
bstring -> binding
2009-03-30, by krauss
code attribute for tailrec-equations, too; tuned
2009-03-30, by krauss
optimistically add code attribute to .simps without further checks
2009-03-30, by krauss
remove "otherwise" feature from function package which was never really documented or used
2009-03-30, by krauss
prep_full_context_statement: explicit record of flags;
2009-03-30, by wenzelm
Limit the number of results returned by auto_solves.
2009-03-30, by Timothy Bourke
merged
2009-03-29, by wenzelm
Merged.
2009-03-29, by ballarin
In interpretation: equations are not propagated through the hierarchy automatically.
2009-03-29, by ballarin
Normalise equation only for morphism, not thm stored in theory.
2009-03-29, by ballarin
Default mode of qualifiers in locale commands.
2009-03-28, by ballarin
Front matter updated.
2009-03-28, by ballarin
tuned;
2009-03-29, by wenzelm
simplified Element.activate(_i): singleton version;
2009-03-29, by wenzelm
tuned;
2009-03-29, by wenzelm
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
2009-03-29, by wenzelm
unified binding prefix terminology;
2009-03-29, by wenzelm
simplified roundup activation interface;
2009-03-29, by wenzelm
merged
2009-03-28, by wenzelm
merged
2009-03-28, by haftmann
merged
2009-03-28, by haftmann
second attempt for code_deps command
2009-03-28, by haftmann
merged
2009-03-28, by haftmann
corrected projection of required statement names
2009-03-28, by haftmann
corrected check for additional type variables on rhs of code equations
2009-03-28, by haftmann
not yet fruitful tex experiments with bounding boxes
2009-03-28, by haftmann
simplified Locale.activate operations, using generic context;
2009-03-28, by wenzelm
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
2009-03-28, by wenzelm
define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;
2009-03-28, by wenzelm
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
2009-03-28, by wenzelm
simplified references to facts, eliminated external note_thmss;
2009-03-28, by wenzelm
added map_facts_refs;
2009-03-28, by wenzelm
tuned;
2009-03-28, by wenzelm
replaced add_binds(_i) by bind_terms -- internal version only;
2009-03-28, by wenzelm
replaced add_binds by singleton bind_term;
2009-03-28, by wenzelm
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-28, by wenzelm
minor tuning;
2009-03-28, by wenzelm
merged
2009-03-28, by wenzelm
Merged.
2009-03-28, by ballarin
Corrections to locale syntax.
2009-03-28, by ballarin
Update explanation of locale expressions to locale reimplementation.
2009-03-27, by ballarin
Comments updated.
2009-03-27, by ballarin
fixed proof
2009-03-27, by chaieb
merged
2009-03-27, by chaieb
fps made instance of number_ring
2009-03-27, by chaieb
updated keywords with polyml-experimental;
2009-03-27, by wenzelm
export position_of;
2009-03-27, by wenzelm
dropped infix union
2009-03-27, by haftmann
tuned notoriously slow metis proof
2009-03-27, by haftmann
merged
2009-03-27, by haftmann
dropped toy example Code_Antiq
2009-03-27, by haftmann
more convenient name uniqueness
2009-03-27, by haftmann
normalized imports
2009-03-27, by haftmann
dropped legacy goal package call
2009-03-27, by haftmann
merged
2009-03-27, by haftmann
merged
2009-03-26, by haftmann
step towards proper pictures in dvi
2009-03-26, by haftmann
merged
2009-03-26, by wenzelm
parameterize assoc_fold with is_numeral predicate
2009-03-26, by huffman
merged
2009-03-26, by paulson
New theorems mostly concerning infinite series.
2009-03-26, by paulson
interpretation/interpret: prefixes are mandatory by default;
2009-03-26, by wenzelm
interpretation/interpret: prefixes are mandatory by default;
2009-03-26, by wenzelm
interpretation/interpret: prefixes within locale expression are mandatory by default;
2009-03-26, by wenzelm
locale_expression: mandatory as parameter;
2009-03-26, by wenzelm
register_locale: produce stamps at the spot where elements are registered;
2009-03-26, by wenzelm
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
2009-03-26, by wenzelm
pretty_thm_aux etc.: explicit show_status flag;
2009-03-26, by wenzelm
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-26, by wenzelm
@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
2009-03-25, by wenzelm
tuned;
2009-03-25, by wenzelm
use more informative Thm.proof_body_of for oracle demo;
2009-03-25, by wenzelm
Proofterm.approximate_proof_body;
2009-03-25, by wenzelm
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
2009-03-25, by wenzelm
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
2009-03-25, by wenzelm
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
2009-03-25, by wenzelm
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
2009-03-24, by wenzelm
status_of: need to include local promises as well!
2009-03-24, by wenzelm
status_of: simultaneous list;
2009-03-24, by wenzelm
display derivation status of thms;
2009-03-24, by wenzelm
recover old ids;
2009-03-24, by wenzelm
report ML typing;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
merged
2009-03-24, by nipkow
NEWS: [arith]
2009-03-24, by nipkow
get_index: produce index of next pending token, not the last one;
2009-03-24, by wenzelm
register token positions persistently with context;
2009-03-24, by wenzelm
tuned;
2009-03-24, by wenzelm
more markup elements for ML programs;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
process at-sml-dev last -- takes very long (why?);
2009-03-24, by wenzelm
fix
2009-03-24, by nipkow
merged
2009-03-24, by nipkow
presburger uses [arith] now
2009-03-24, by nipkow
merged
2009-03-24, by wenzelm
merged
2009-03-24, by haftmann
added Imperative_HOL_ex
2009-03-24, by haftmann
Use assms rather than prems in find_theorems solves.
2009-03-24, by Timothy Bourke
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
2009-03-23, by huffman
lemmas add_sign_intros
2009-03-23, by huffman
merged
2009-03-23, by haftmann
moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-23, by haftmann
corrected variable renaming
2009-03-23, by haftmann
tuned error messages
2009-03-23, by haftmann
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-23, by haftmann
structure LinArith now named Lin_Arith
2009-03-23, by haftmann
suddenly infix identifier oo occurs in generated code
2009-03-23, by haftmann
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-24, by wenzelm
eliminated non-canonical alias structure T = ML_Lex;
2009-03-24, by wenzelm
error "Static Errors";
2009-03-24, by wenzelm
more systematic type use_context;
2009-03-24, by wenzelm
tuned;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
eliminated Output.ml_output;
2009-03-23, by wenzelm
pretty_ml/ml_pretty: proper handling of markup and string length;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
removed obsolete ml_output;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-23, by wenzelm
de-camelized ML_Name_Space;
2009-03-23, by wenzelm
suppress status output for traditional tty modes (including Proof General);
2009-03-23, by wenzelm
added report_text -- status messages with text body;
2009-03-23, by wenzelm
maintain parse trees cumulatively;
2009-03-23, by wenzelm
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
2009-03-23, by wenzelm
future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
2009-03-23, by wenzelm
merged
2009-03-23, by haftmann
Main is (Complex_Main) base entry point in library theories
2009-03-23, by haftmann
Main is (Complex_Main) base entry point in library theories
2009-03-23, by haftmann
added instances for bot, top, wellorder
2009-03-23, by haftmann
tuned header
2009-03-23, by haftmann
more canonical import, syntax fix
2009-03-23, by haftmann
merged
2009-03-23, by haftmann
merged
2009-03-22, by haftmann
more antiquotations
2009-03-22, by haftmann
moved import of module qelim to theory Presburger
2009-03-22, by haftmann
tuned header
2009-03-22, by haftmann
dropped theory Arith_Tools
2009-03-22, by haftmann
lemma nat_dvd_not_less moved here from Arith_Tools
2009-03-22, by haftmann
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-22, by haftmann
merged
2009-03-22, by wenzelm
merged
2009-03-22, by nipkow
1. New cancellation simprocs for common factors in inequations
2009-03-22, by nipkow
clarified relationship of modules Code_Name and Code_Printer
2009-03-22, by haftmann
added Symreltab (binary relations of symbols) instance of TableFun
2009-03-22, by haftmann
proper signature;
2009-03-22, by wenzelm
added read_antiq, with improved error reporting;
2009-03-22, by wenzelm
ML_Lex.read_antiq;
2009-03-22, by wenzelm
ML_Lex.read_antiq;
2009-03-22, by wenzelm
simplified Antiquote.read (again);
2009-03-22, by wenzelm
export report -- version that actually covers all cases;
2009-03-22, by wenzelm
Test of advanced ML compiler invocation in Poly/ML 5.3.
2009-03-22, by wenzelm
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
2009-03-22, by wenzelm
added pretty_ml;
2009-03-22, by wenzelm
export eval_antiquotes: refined version that operates on ML tokens;
2009-03-22, by wenzelm
ML_Lex.pos_of: regular position;
2009-03-22, by wenzelm
replaced Antiquote.is_antiq by Antiquote.is_text;
2009-03-22, by wenzelm
merged
2009-03-21, by wenzelm
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
2009-03-21, by wenzelm
merged
2009-03-21, by wenzelm
merged
2009-03-21, by huffman
move field lemmas into class locale context
2009-03-21, by huffman
move diff_eq_0_iff_eq into class locale context
2009-03-21, by huffman
removed obsolete pprint operations;
2009-03-21, by wenzelm
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
2009-03-21, by wenzelm
adapted toplevel_pp to ML_Pretty.pretty;
2009-03-21, by wenzelm
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
2009-03-21, by wenzelm
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
2009-03-21, by wenzelm
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
2009-03-21, by wenzelm
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
2009-03-21, by wenzelm
Pretty.position;
2009-03-21, by wenzelm
added position;
2009-03-21, by wenzelm
added generic ML_Pretty interface;
2009-03-21, by wenzelm
restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
2009-03-21, by wenzelm
more ambitious ML_OPTIONS;
2009-03-21, by wenzelm
more stats;
2009-03-21, by wenzelm
added ML syntax markup;
2009-03-20, by wenzelm
report markup for ML tokens;
2009-03-20, by wenzelm
Antiquote.read: argument for reporting text;
2009-03-20, by wenzelm
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
2009-03-20, by wenzelm
uniform ml_prompts for RAW and Pure;
2009-03-20, by wenzelm
eliminated old Addsimps;
2009-03-20, by wenzelm
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-20, by wenzelm
fixed possibility_tac;
2009-03-20, by wenzelm
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-20, by wenzelm
merged
2009-03-20, by wenzelm
merged
2009-03-20, by berghofe
split_codegen now eta-expands terms on-the-fly.
2009-03-20, by berghofe
proper context for prove_cont/adm_tac;
2009-03-20, by wenzelm
with_attributes: canonical capture/release scheme (potentially iron out race condition);
2009-03-20, by wenzelm
considerable speedup of benchmarks by using minimal simpset;
2009-03-20, by wenzelm
allow non-printable symbols within string tokens;
2009-03-20, by wenzelm
merged
2009-03-19, by wenzelm
add lemma det_diagonal; remove wellorder requirement on several lemmas
2009-03-19, by huffman
merged
2009-03-19, by haftmann
tuned some theorem and attribute bindings
2009-03-19, by haftmann
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-19, by wenzelm
eval_antiquotes: joint scanning of ML tokens and antiquotations;
2009-03-19, by wenzelm
added scan_antiq;
2009-03-19, by wenzelm
RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
2009-03-19, by wenzelm
added tokenize;
2009-03-19, by wenzelm
parameterized datatype antiquote and read operation;
2009-03-19, by wenzelm
Antiquote.Text: keep full position information;
2009-03-19, by wenzelm
OuterLex.read_antiq;
2009-03-19, by wenzelm
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
2009-03-19, by wenzelm
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
2009-03-19, by wenzelm
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-19, by wenzelm
Name.of_binding: proper full_name (with checks) before projecting base name;
2009-03-19, by wenzelm
merged
2009-03-19, by wenzelm
imported patch euclidean
2009-03-19, by huffman
Merged.
2009-03-18, by ballarin
Updated chapters 1-5 to locale reimplementation.
2009-03-18, by ballarin
command 'use', 'ML': apply ML environment to theory and target as well;
2009-03-19, by wenzelm
added map_contexts (cf. Proof.map_contexts);
2009-03-19, by wenzelm
tuned;
2009-03-19, by wenzelm
generalized ML_Context.inherit_env;
2009-03-18, by wenzelm
more precise type Symbol_Pos.text;
2009-03-18, by wenzelm
more precise type Symbol_Pos.text;
2009-03-18, by wenzelm
de-camelized Symbol_Pos;
2009-03-18, by wenzelm
Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
2009-03-18, by wenzelm
reduced verbosity;
2009-03-18, by wenzelm
made SML/NJ happy
2009-03-18, by haftmann
tuned interpunctation
2009-03-18, by haftmann
strip_abss: always strip abstractions as far as possible, without keeping alternatives (which appear to be redundant anyway, but cause significant slowdown since discrimination nets collapse abstractions);
2009-03-17, by wenzelm
close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
2009-03-17, by wenzelm
reverted abbreviations: improved performance via Item_Net.T;
2009-03-17, by wenzelm
export match_rew -- useful for implementing "procs" for rewrite_term;
2009-03-17, by wenzelm
tuned comment;
2009-03-17, by wenzelm
merged
2009-03-17, by wenzelm
document new additions to HOL/Library
2009-03-16, by huffman
clean up proofs
2009-03-16, by huffman
adapted to general Item_Net;
2009-03-17, by wenzelm
turned structure NetRules into general Item_Net, which is loaded earlier;
2009-03-17, by wenzelm
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2009-03-17, by wenzelm
goal_tac: finish marked assumptions from left to right -- corresponds better with the strategy of etac, with significant performance gains in some situations;
2009-03-17, by wenzelm
eq_assumption: slightly more efficient by checking (open) result of Logic.assum_problems directly;
2009-03-17, by wenzelm
tuned aeconv: test plain aconv before expensive eta_contract;
2009-03-17, by wenzelm
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
2009-03-16, by wenzelm
refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
2009-03-16, by wenzelm
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-03-16, by wenzelm
method parser: pass proper context;
2009-03-16, by wenzelm
merged
2009-03-16, by wenzelm
simplified method setup;
2009-03-16, by wenzelm
updated generated file;
2009-03-16, by wenzelm
simplifief 'method_setup' command;
2009-03-16, by wenzelm
spelling;
2009-03-16, by wenzelm
export method parser;
2009-03-16, by wenzelm
adapted 'method_setup' command to Method.setup;
2009-03-16, by wenzelm
tuned signature;
2009-03-16, by wenzelm
have remote script interrupted like the other provers
2009-03-16, by immler
simplified method setup;
2009-03-15, by wenzelm
export section, sections;
2009-03-15, by wenzelm
merged
2009-03-15, by wenzelm
updated NEWS
2009-03-14, by immler
use goal instead of Proof State
2009-03-14, by immler
split relevance-filter and writing of problem-files;
2009-03-14, by immler
show certain errors to the user
2009-03-14, by immler
removed connection check;
2009-03-14, by immler
merged
2009-03-15, by wenzelm
merged
2009-03-14, by haftmann
reverted to old version of Set.thy -- strange effects have to be traced first
2009-03-14, by haftmann
simplified attribute and method setup;
2009-03-15, by wenzelm
simplified attribute setup;
2009-03-15, by wenzelm
simplified attribute setup;
2009-03-15, by wenzelm
updated generated files;
2009-03-15, by wenzelm
added 'attribute_setup' command;
2009-03-15, by wenzelm
added setup and attribute_setup -- expect plain parser instead of syntax function;
2009-03-15, by wenzelm
ML_Syntax.make_binding;
2009-03-15, by wenzelm
added make_binding;
2009-03-15, by wenzelm
removed obsolete no_base_names naming policy;
2009-03-14, by wenzelm
merged
2009-03-13, by wenzelm
merged
2009-03-13, by haftmann
coherent binding policy with primitive target operations
2009-03-13, by haftmann
moved some generic nonsense to arith_data.ML
2009-03-13, by haftmann
tuned ML code
2009-03-13, by haftmann
remove legacy ML bindings
2009-03-13, by huffman
simplified method setup;
2009-03-13, by wenzelm
simplified goal_spec: default to first goal;
2009-03-13, by wenzelm
eliminated type Args.T;
2009-03-13, by wenzelm
added simplified setup;
2009-03-13, by wenzelm
pervasive types 'a parser and 'a context_parser;
2009-03-13, by wenzelm
unified type Proof.method and pervasive METHOD combinators;
2009-03-13, by wenzelm
more regular method setup via SIMPLE_METHOD;
2009-03-13, by wenzelm
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
2009-03-13, by wenzelm
merged
2009-03-13, by wenzelm
fix typed print translation for CARD('a)
2009-03-13, by huffman
introduce new helper functions; clean up proofs
2009-03-13, by huffman
merged
2009-03-13, by nipkow
added comment
2009-03-13, by nipkow
hiding numeric coercions in LaTeX
2009-03-13, by nipkow
merged
2009-03-13, by haftmann
dropped spurious `quote` tags
2009-03-13, by haftmann
merged
2009-03-12, by haftmann
tuned
2009-03-12, by haftmann
strippd Id
2009-03-12, by haftmann
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-03-12, by haftmann
tuned
2009-03-12, by haftmann
consider exit status of code generation direcitve
2009-03-12, by haftmann
provide regular ML interfaces for Isar source language elements;
2009-03-13, by wenzelm
get data from plain Proof.context;
2009-03-13, by wenzelm
more user aliases;
2009-03-12, by wenzelm
merged
2009-03-12, by wenzelm
remove trailing spaces
2009-03-12, by huffman
remove trailing spaces
2009-03-12, by huffman
simplified preparation and outer parsing of specification;
2009-03-12, by wenzelm
simplified preparation and outer parsing of specification;
2009-03-12, by wenzelm
removed legacy_infer_term, legacy_infer_prop;
2009-03-12, by wenzelm
old name_spec for 'axioms' and 'defs' (from spec_parse.ML);
2009-03-12, by wenzelm
added legacy type inference (from fixrec_package.ML);
2009-03-12, by wenzelm
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
2009-03-12, by wenzelm
removed old named_spec, spec_name, spec_opt_name;
2009-03-12, by wenzelm
keep dead code fresh;
2009-03-12, by wenzelm
tuned;
2009-03-12, by wenzelm
merged
2009-03-12, by wenzelm
merged
2009-03-12, by nipkow
added div lemmas
2009-03-12, by nipkow
merged
2009-03-12, by nipkow
optional latex sugar
2009-03-12, by nipkow
Assumption.all_prems_of, Assumption.all_assms_of;
2009-03-12, by wenzelm
Assumption.local_prems_of;
2009-03-12, by wenzelm
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
2009-03-12, by wenzelm
axiomatization: more precise treatment of binding;
2009-03-12, by wenzelm
renamed sticky_prefix to mandatory_path;
2009-03-12, by wenzelm
replaced old-style add_path/no_base_names by sticky_prefix;
2009-03-12, by wenzelm
updated according to actual manual title;
2009-03-12, by wenzelm
renamed NameSpace.bind to NameSpace.define;
2009-03-12, by wenzelm
renamed bind to define;
2009-03-12, by wenzelm
tuned signature;
2009-03-12, by wenzelm
updated generated files;
2009-03-12, by wenzelm
tuned;
2009-03-12, by wenzelm
added 'local_setup' command;
2009-03-11, by wenzelm
debugging: special handling of EXCURSION_FAIL;
2009-03-11, by wenzelm
tuned;
2009-03-11, by wenzelm
delete unused generated files;
2009-03-11, by wenzelm
basic setup for "main" as generated Isabelle manual;
2009-03-11, by wenzelm
tuned;
2009-03-11, by wenzelm
merged
2009-03-11, by wenzelm
merged
2009-03-11, by haftmann
fixed typo
2009-03-11, by haftmann
(restored previous version)
2009-03-11, by haftmann
corrected type inference of primitive definitions
2009-03-11, by haftmann
HOLogic.mk_set, HOLogic.dest_set
2009-03-11, by haftmann
tuned
2009-03-11, by haftmann
tuned funny error message
2009-03-11, by haftmann
stripped dead code
2009-03-11, by haftmann
min_weak_def [code del]
2009-03-11, by haftmann
renamed (unused?) "split.splits" to split_splits -- it was only accepted by accident;
2009-03-11, by wenzelm
merged
2009-03-11, by wenzelm
Extended approximation boundaries by fractions and base-2 floating point numbers
2009-03-11, by hoelzl
Added "What's in Main" to doc sources
2009-03-11, by nipkow
merged
2009-03-11, by nipkow
Docs
2009-03-11, by nipkow
Updated paths in Decision_Procs comments and NEWS
2009-03-11, by hoelzl
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
2009-03-11, by wenzelm
more precise treatment of qualified bindings;
2009-03-11, by wenzelm
removed obsolete absolute_path -- use root_path with qualified binding;
2009-03-11, by wenzelm
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
2009-03-11, by wenzelm
Thm.def_binding_optional;
2009-03-11, by wenzelm
added def_binding_optional -- robust version of def_name_optional for bindings;
2009-03-11, by wenzelm
merged
2009-03-11, by haftmann
avoid inspecting pretty output
2009-03-11, by haftmann
explicit code equations for some rarely used pred operations
2009-03-11, by haftmann
moved Decision_Procs examples to Decision_Procs/ex
2009-03-11, by haftmann
explicitly delete some code equations
2009-03-11, by haftmann
delete code equations for types pred and seq
2009-03-11, by haftmann
merged
2009-03-10, by wenzelm
Docs
2009-03-10, by nipkow
Consts.eq_const is back again (cf. 907da436f8a9) -- required in ProofContext.transfer_syntax to prevent expensive merges of local_consts/global_consts;
2009-03-10, by wenzelm
recover old ids;
2009-03-10, by wenzelm
controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;
2009-03-10, by wenzelm
explicit root_path, parent_path;
2009-03-10, by wenzelm
removed obsolete no_base_names;
2009-03-10, by wenzelm
invoke_case: proper qualification of name binding, avoiding old no_base_names;
2009-03-10, by wenzelm
add_path: discontinued special meaning of "//", "/", "..";
2009-03-10, by wenzelm
merged
2009-03-10, by wenzelm
Automated merge with ssh://webertj@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-10, by webertj
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-10, by webertj
merged
2009-03-10, by wenzelm
Fixed type error which appeared when Approximation bounds where specified as floating point numbers
2009-03-10, by hoelzl
just one naming policy based on binding content -- eliminated odd "object-oriented" style;
2009-03-10, by wenzelm
tuned proofs;
2009-03-10, by wenzelm
added qualified_name_of;
2009-03-10, by wenzelm
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-10, by wenzelm
quote binding for ML toplevel pp;
2009-03-10, by wenzelm
merged
2009-03-10, by wenzelm
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-10, by webertj
updated generated file -- changed due to different treatmeant of type constraints in OptionalSugar.thy;
2009-03-10, by wenzelm
more robust treatment of (authentic) consts within translations;
2009-03-10, by wenzelm
Docs
2009-03-09, by nipkow
merged
2009-03-09, by nipkow
Docs
2009-03-09, by nipkow
added session HOL-Docs;
2009-03-09, by wenzelm
tuned;
2009-03-09, by wenzelm
simplified presentation_context_of;
2009-03-09, by wenzelm
markup antiquotation options;
2009-03-09, by wenzelm
fornal markup for antiquotation options;
2009-03-09, by wenzelm
* More systematic treatment of long names, abstract name bindings, and name space operations.
2009-03-09, by wenzelm
moved @{ML_functor} and @{ML_text} to Pure;
2009-03-09, by wenzelm
replaced old locale option by proper "text (in locale)";
2009-03-09, by wenzelm
adapted to simplified ThyOutput.antiquotation interface;
2009-03-09, by wenzelm
adapted to simplified ThyOutput.antiquotation interface;
2009-03-09, by wenzelm
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
2009-03-09, by wenzelm
merged
2009-03-09, by wenzelm
merged
2009-03-09, by haftmann
NameSpace.base_name ~> Long_Name.base_name
2009-03-09, by haftmann
Docs
2009-03-09, by nipkow
merged
2009-03-09, by nipkow
fixed typing of UN/INT syntax
2009-03-09, by nipkow
more contributors;
2009-03-09, by wenzelm
adapted ThyOutput.antiquotation;
2009-03-09, by wenzelm
refined antiquotation interface: formally pass result context and (potential) result source;
2009-03-09, by wenzelm
merged
2009-03-09, by haftmann
binding replaces bstring
2009-03-09, by haftmann
dropped eq_pred
2009-03-09, by haftmann
merged
2009-03-08, by haftmann
refined enumeration implementation
2009-03-08, by haftmann
added top and bot syntax
2009-03-08, by haftmann
added predicate compiler, as formally checked prototype, not as user package
2009-03-08, by haftmann
attempt to bypass spurious infix syntax problem on polyml/sun
2009-03-09, by haftmann
UN syntax fix
2009-03-09, by nipkow
merged
2009-03-09, by nipkow
Docs updates
2009-03-09, by nipkow
use simplified ThyOutput.antiquotation;
2009-03-08, by wenzelm
added (raw_)antiquotation -- simplified wrapper for defining output commands;
2009-03-08, by wenzelm
simplified presentation: pass state directly;
2009-03-08, by wenzelm
simplified presentation: built into transaction, pass state directly;
2009-03-08, by wenzelm
adapted to structure Long_Name;
2009-03-08, by wenzelm
moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-08, by wenzelm
proper local context for text with antiquotations;
2009-03-08, by wenzelm
more explicit warning message;
2009-03-08, by wenzelm
added qualified_name -- emulates old-style qualified bstring;
2009-03-08, by wenzelm
added General/long_name.ML;
2009-03-08, by wenzelm
moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-08, by wenzelm
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
2009-03-08, by wenzelm
proper context for Simplifier.pretty_ss;
2009-03-08, by wenzelm
added dest_ss;
2009-03-08, by wenzelm
use binding type;
2009-03-08, by wenzelm
merged
2009-03-08, by wenzelm
merged
2009-03-07, by haftmann
restructured theory Set.thy
2009-03-07, by haftmann
merged
2009-03-07, by wenzelm
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
2009-03-07, by blanchet
Added a second timeout mechanism to Refute.
2009-03-07, by blanchet
merged
2009-03-07, by blanchet
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
2009-03-07, by blanchet
minimal adaptions for abstract binding type;
2009-03-07, by wenzelm
more uniform handling of binding in packages;
2009-03-07, by wenzelm
more uniform handling of binding in targets and derived elements;
2009-03-07, by wenzelm
replace old bstring by binding for logical primitives: class, type, const etc.;
2009-03-07, by wenzelm
moved Thm.def_name(_optional) to more_thm.ML;
2009-03-07, by wenzelm
adapted Syntax.const_name;
2009-03-07, by wenzelm
canonical argument order for type_name, const_name;
2009-03-07, by wenzelm
added const_binding;
2009-03-07, by wenzelm
added prefix_name, suffix_name;
2009-03-07, by wenzelm
Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-07, by wenzelm
renamed rep_ss to MetaSimplifier.internal_ss;
2009-03-07, by wenzelm
Binding.str_of: removed verbose feature, include qualifier in output;
2009-03-07, by wenzelm
oracle: proper name position, tuned;
2009-03-07, by wenzelm
merged
2009-03-07, by haftmann
drop poisonous code equations
2009-03-07, by haftmann
suppress document output
2009-03-07, by haftmann
theory with syntax for lattice operations
2009-03-06, by haftmann
added babel -- necessary for bind infix syntax
2009-03-06, by haftmann
added enumeration of predicates
2009-03-06, by haftmann
moved instance option :: finite to Option.thy
2009-03-06, by haftmann
constructive version of Cantor's first diagonalization argument
2009-03-06, by haftmann
equalities for Min, Max
2009-03-06, by haftmann
merged
2009-03-06, by wenzelm
added lemma
2009-03-06, by nipkow
merged
2009-03-06, by nipkow
Docs
2009-03-06, by nipkow
eliminated Output.immediate_output -- violates the official message channel protocol;
2009-03-06, by wenzelm
schedule_seq: handle after_load errors as in schedule_futures;
2009-03-06, by wenzelm
replaced archaic use of rep_ss by Simplifier.mksimps;
2009-03-06, by wenzelm
improved error handling for document antiquotations;
2009-03-06, by wenzelm
merged
2009-03-06, by blanchet
merged
2009-03-06, by nipkow
Added "expect" option to Refute, like in Nitpick, that allows to write regression tests.
2009-03-06, by blanchet
added lemmas
2009-03-06, by nipkow
Fix remaining occurrences of "'a set" in Refute, by using "'a => bool" instead.
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
merged
2009-03-06, by blanchet
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
2009-03-06, by blanchet
merged
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-06, by haftmann
merged
2009-03-05, by haftmann
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-05, by haftmann
tuned
2009-03-05, by haftmann
moved complete_lattice to Set.thy
2009-03-05, by haftmann
dropped Id
2009-03-05, by haftmann
corrected slip in NEWS
2009-03-06, by haftmann
merged
2009-03-06, by haftmann
added strict_mono predicate
2009-03-06, by haftmann
Identifiers of some old CVS file versions;
2009-03-06, by wenzelm
recovered generated files;
2009-03-06, by wenzelm
more precise deps;
2009-03-06, by wenzelm
merged
2009-03-06, by nipkow
Added Docs
2009-03-06, by nipkow
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
2009-03-05, by wenzelm
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
2009-03-05, by wenzelm
removed unused TableFun().fold_map and GraphFun().fold_map_nodes;
2009-03-05, by wenzelm
removed spurious occurrences of old rep_ss;
2009-03-05, by wenzelm
Thm.add_oracle interface: replaced old bstring by binding;
2009-03-05, by wenzelm
silent chmod;
2009-03-05, by wenzelm
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
2009-03-05, by wenzelm
close_schematic_term: uniform order of types/terms;
2009-03-05, by wenzelm
eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
2009-03-05, by wenzelm
TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
2009-03-05, by wenzelm
fixed proofs -- follow-up to ecd6f0ca62ea;
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
2009-03-05, by wenzelm
renamed NameSpace.base to NameSpace.base_name;
2009-03-05, by wenzelm
eliminated obsolete ProofContext.full_bname;
2009-03-05, by wenzelm
Binding.prefix_of;
2009-03-05, by wenzelm
adapted Binding.dest;
2009-03-05, by wenzelm
added prefix_of;
2009-03-05, by wenzelm
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-05, by blanchet
merged
2009-03-05, by wenzelm
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04, by huffman
regenerated document;
2009-03-05, by wenzelm
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
2009-03-05, by wenzelm
dummy changes to produce a new changeset of these files;
2009-03-05, by wenzelm
updated generated file -- changed since @{ML} now ignores source flag;
2009-03-05, by wenzelm
fixed document;
2009-03-05, by wenzelm
removed old/broken CVS Ids;
2009-03-04, by wenzelm
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
2009-03-04, by wenzelm
merged
2009-03-04, by chaieb
Moved general theorems about sums and products to FiniteSet.thy
2009-03-04, by chaieb
fixed proofs; added rules as default simp-rules
2009-03-04, by chaieb
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
2009-03-04, by chaieb
Added Libray dependency on Topology_Euclidean_Space
2009-03-04, by chaieb
Added general theorems for fold_image, setsum and set_prod
2009-03-04, by chaieb
fixed proofs
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-03-04, by chaieb
merged
2009-02-25, by chaieb
merged
2009-02-25, by chaieb
Second try at adding "nitpick_const_def" attribute.
2009-03-04, by blanchet
Fix parentheses.
2009-03-04, by blanchet
merged
2009-03-04, by blanchet
Added "nitpick_const_simp" attribute to Nominal primrec.
2009-03-04, by blanchet
NEWS: renamed o2s to Option.set;
2009-03-04, by wenzelm
less arbitrary occurrences of undefined
2009-03-04, by haftmann
datatype antiquotation does not assume LaTeX as output any longer
2009-03-04, by haftmann
merged
2009-03-04, by nipkow
Option.thy
2009-03-04, by nipkow
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
2009-03-04, by haftmann
merged
2009-03-04, by haftmann
explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-04, by haftmann
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Merge.
2009-03-04, by blanchet
Made Refute.norm_rhs public, so I can use it in Nitpick.
2009-03-04, by blanchet
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
2009-03-01, by blanchet
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
2009-02-24, by blanchet
merged
2009-03-04, by nipkow
Made Option a separate theory and renamed option_map to Option.map
2009-03-04, by nipkow
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
2009-03-04, by wenzelm
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
2009-03-03, by wenzelm
tuned str_of, now subject to verbose flag;
2009-03-03, by wenzelm
added @{binding} ML antiquotations;
2009-03-03, by wenzelm
added print_properties, print_position (again);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
merged
2009-03-03, by haftmann
tuned manuals
2009-03-03, by haftmann
more canonical directory structure of manuals
2009-03-03, by haftmann
merged
2009-03-03, by wenzelm
removed and renamed redundant lemmas
2009-03-03, by nipkow
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03, by wenzelm
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
2009-03-03, by wenzelm
added markup for binding;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
Binding.str_of;
2009-03-03, by wenzelm
renamed Binding.display to Binding.str_of, which is slightly more canonical;
2009-03-03, by wenzelm
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
moved name space externalization flags back to name_space.ML;
2009-03-03, by wenzelm
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
2009-03-03, by wenzelm
merged
2009-03-03, by wenzelm
Thm.binding;
2009-03-03, by wenzelm
added type binding and val empty_binding;
2009-03-03, by wenzelm
updated generated files;
2009-03-03, by wenzelm
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
2009-03-03, by wenzelm
Implement Makarius's suggestion for improved type pattern parsing.
2009-03-03, by Timothy Bourke
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
2009-03-02, by Timothy Bourke
adapted to lates experimental version;
2009-03-02, by wenzelm
removed Ids;
2009-03-02, by wenzelm
merged
2009-03-02, by haftmann
reduced confusion code_funcgr vs. code_wellsorted
2009-03-02, by haftmann
better markup
2009-03-02, by haftmann
name fix
2009-03-02, by nipkow
merged
2009-03-02, by nipkow
name changes
2009-03-02, by nipkow
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-02, by chaieb
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
2009-03-02, by chaieb
fixed broken @{file} refs;
2009-03-02, by wenzelm
merged
2009-03-02, by wenzelm
using plain ISABELLE_PROCESS
2009-03-02, by haftmann
merged
2009-03-02, by haftmann
ignore ISABELLE_LINE_EDITOR for code generation
2009-03-02, by haftmann
use long names for old-style fold combinators;
2009-03-01, by wenzelm
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-03-01, by wenzelm
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-03-01, by wenzelm
end_timing: generalized result -- message plus with explicit time values;
2009-03-01, by wenzelm
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
2009-03-01, by wenzelm
updated contributors;
2009-03-01, by wenzelm
removed parts of the manual that are clearly obsolete, or covered by
2009-03-01, by wenzelm
merged
2009-03-01, by wenzelm
minor update of Mercurial HOWTO;
2009-03-01, by wenzelm
removed redundant lemmas
2009-03-01, by nipkow
added lemmas by Jeremy Avigad
2009-03-01, by nipkow
A Serbian theory, by Filip Maric.
2009-02-28, by wenzelm
more accurate deps;
2009-02-28, by wenzelm
merged
2009-02-28, by wenzelm
add news for HOLCF; fixed some typos and inaccuracies
2009-02-28, by huffman
fixed headers;
2009-02-28, by wenzelm
moved isabelle_system.scala to src/Pure/System/;
2009-02-28, by wenzelm
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-28, by wenzelm
updated generated files;
2009-02-28, by wenzelm
added method "coherent";
2009-02-28, by wenzelm
more refs;
2009-02-28, by wenzelm
moved method "iprover" to HOL specific part;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
simultaneous use_thys;
2009-02-28, by wenzelm
replaced low-level 'no_syntax' by 'no_notation';
2009-02-28, by wenzelm
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
2009-02-28, by wenzelm
tuned message;
2009-02-28, by wenzelm
* New prover for coherent logic (see src/Tools/coherent.ML).
2009-02-28, by wenzelm
more CONTRIBUTORS;
2009-02-28, by wenzelm
removed Ids;
2009-02-28, by wenzelm
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
2009-02-28, by wenzelm
some updates on ancient README;
2009-02-28, by wenzelm
fixrec package uses new-style syntax and local-theory interface
2009-02-27, by huffman
add function taken_names
2009-02-27, by huffman
merged
2009-02-27, by huffman
make list-style polynomial syntax work when show_sorts is on
2009-02-27, by huffman
more CONTRIBUTORS;
2009-02-27, by wenzelm
turned "read-only refs" typ_level and minimize_applies into constant values;
2009-02-27, by wenzelm
merged
2009-02-27, by wenzelm
removed global ref dfg_format
2009-02-26, by immler
removed local ref const_needs_hBOOL;
2009-02-25, by immler
removed local ref const_min_arity
2009-02-24, by immler
eliminated private clones of List.partition;
2009-02-27, by wenzelm
observe some Isabelle/ML coding conventions;
2009-02-27, by wenzelm
eliminated NJ's List.nth;
2009-02-27, by wenzelm
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
2009-02-27, by wenzelm
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
2009-02-27, by wenzelm
observe basic Isabelle/ML coding conventions;
2009-02-27, by wenzelm
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
2009-02-27, by wenzelm
added ML-Systems/polyml-experimental.ML;
2009-02-27, by wenzelm
tuned;
2009-02-27, by wenzelm
even less default memory for sunbroy2;
2009-02-27, by wenzelm
merged
2009-02-27, by boehmes
merged
2009-02-27, by boehmes
Made then_conv and else_conv available as infix operations.
2009-02-26, by boehmes
merged
2009-02-27, by haftmann
fixed typo
2009-02-27, by haftmann
merged
2009-02-26, by huffman
avoid using legacy type inference
2009-02-26, by huffman
use TheoryData to keep track of pattern match combinators
2009-02-26, by huffman
merged
2009-02-26, by huffman
remove unnecessary simp rules
2009-02-26, by huffman
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
2009-02-26, by huffman
merged
2009-02-26, by wenzelm
back to canonical ROOT, to see if memory problems still persist;
2009-02-26, by wenzelm
trying less default memory for sunbroy2 test
2009-02-27, by kleing
basic setup for chapter "Syntax and type-checking";
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
standard headers;
2009-02-26, by wenzelm
updated generated files;
2009-02-26, by wenzelm
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
2009-02-26, by wenzelm
fixed import of ~~/src/HOL/Decision_Procs/Ferrack;
2009-02-26, by wenzelm
more explicit indication of old manuals;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
\bibliographystyle{abbrv} for newer ref manuals;
2009-02-26, by wenzelm
added Haftmann-Wenzel:2009;
2009-02-26, by wenzelm
updated generated files;
2009-02-26, by wenzelm
isabelle document: adapted (postulated) defaults for tags to actual isabelle.sty;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
include HOL-Decision_Procs in stats;
2009-02-26, by wenzelm
back to plain http;
2009-02-26, by wenzelm
merged
2009-02-26, by berghofe
Added postprocessing rules for fresh_star.
2009-02-26, by berghofe
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
2009-02-26, by berghofe
tuned NEWS;
2009-02-26, by wenzelm
merged
2009-02-26, by wenzelm
merged
2009-02-26, by huffman
add type annotation
2009-02-26, by huffman
disable floor_minus and ceiling_minus [simp]
2009-02-26, by huffman
merged
2009-02-26, by wenzelm
merged
2009-02-26, by paulson
Updated the theory syntax. Corrected an error in a command.
2009-02-26, by paulson
merged
2009-02-25, by huffman
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
2009-02-25, by huffman
new theory of Archimedean fields
2009-02-25, by huffman
add lemmas about comparisons of Fract a b with 0 and 1
2009-02-25, by huffman
merged
2009-02-25, by huffman
add lemma diff_Suc_1
2009-02-25, by huffman
Added lemmas for normalizing freshness results involving fresh_star.
2009-02-25, by berghofe
Added typing and evaluation relations, together with proofs of preservation
2009-02-25, by berghofe
merged
2009-02-25, by berghofe
Use LocalTheory.full_name instead of Sign.full_name, because the latter does
2009-02-25, by berghofe
Replaced Logic.unvarify by Variable.import_terms to make declaration of
2009-02-25, by berghofe
nominal_inductive and equivariance now work on local_theory.
2009-02-25, by berghofe
Added equivariance lemmas for fresh_star.
2009-02-25, by berghofe
NEWS
2009-02-25, by nipkow
merged
2009-02-25, by haftmann
robustified
2009-02-25, by haftmann
make more proofs work whether or not One_nat_def is a simp rule
2009-02-24, by huffman
add simp rules for numerals with 1::nat
2009-02-24, by huffman
fix lemma hypreal_hnorm_def
2009-02-24, by huffman
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-23, by huffman
move lemma dvd_mod_imp_dvd into class semiring_div
2009-02-23, by huffman
merged
2009-02-23, by haftmann
improved treatment of case certificates
2009-02-23, by haftmann
repaired order of variable node allocation
2009-02-23, by haftmann
explicitly import Fact
2009-02-23, by huffman
change imports to move Fact.thy outside Plain
2009-02-23, by huffman
add lemmas poly_{div,mod}_minus_{left,right}
2009-02-23, by huffman
merged
2009-02-23, by huffman
declare scaleR distrib rules [algebra_simps]; cleaned up
2009-02-22, by huffman
clean up instantiations
2009-02-22, by huffman
merged
2009-02-22, by huffman
simplify some proofs
2009-02-22, by huffman
remove duplicate instance declaration
2009-02-22, by huffman
stripped classrels_of, instances_of
2009-02-23, by haftmann
use canonical subalgebra projection
2009-02-23, by haftmann
experimental switch to new well-sorting algorithm
2009-02-22, by haftmann
handle NONE case in arity function properly
2009-02-22, by haftmann
clarified status of variables in evaluation terms; tuned header
2009-02-22, by haftmann
subalgebra: drop arities if desired
2009-02-22, by haftmann
merged
2009-02-22, by haftmann
more liberality needed
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
added lemmas
2009-02-22, by nipkow
merged
2009-02-22, by haftmann
simplified evaluation
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
added dvd_div_mult
2009-02-22, by nipkow
merged
2009-02-22, by haftmann
first attempt to solve evaluation bootstrap problem
2009-02-22, by haftmann
formal dependency on newly emerging algorithm
2009-02-22, by haftmann
merged
2009-02-22, by nipkow
name fix
2009-02-22, by nipkow
fix spelling
2009-02-21, by huffman
real_inner class instance for vectors
2009-02-21, by huffman
NEWS
2009-02-21, by nipkow
merged
2009-02-21, by nipkow
Removed subsumed lemmas
2009-02-21, by nipkow
remove duplicated lemmas about norm
2009-02-21, by huffman
real_normed_vector instance
2009-02-21, by huffman
fix real_vector, real_algebra instances
2009-02-21, by huffman
merged
2009-02-21, by huffman
generalize lemmas from nat to 'a::wellorder
2009-02-20, by huffman
generalize some lemmas
2009-02-20, by huffman
merged
2009-02-21, by nipkow
removed redundant thms
2009-02-21, by nipkow
merged
2009-02-20, by huffman
class instances for num1
2009-02-20, by huffman
Removed redundant lemmas
2009-02-20, by nipkow
merged
2009-02-20, by haftmann
also consider superclasses properly
2009-02-20, by haftmann
merged
2009-02-20, by nipkow
removed subsumed lemmas
2009-02-20, by nipkow
merged
2009-02-20, by haftmann
datatype antiquotation: always bracket types with spaces in between
2009-02-20, by haftmann
consequent use of term `code equation`
2009-02-20, by haftmann
permissive check for pattern discipline in case schemes
2009-02-20, by haftmann
maintain order of constructors in datatypes; clarified conventions for type schemes
2009-02-20, by haftmann
stripped Id
2009-02-20, by haftmann
merged
2009-02-20, by huffman
add theory of products as real vector spaces to Library
2009-02-20, by huffman
add new theory Product_plus.thy to Library
2009-02-20, by huffman
merged
2009-02-20, by immler
changed message
2009-02-20, by immler
detailed information on atp-failure via Output.debug
2009-02-20, by immler
merged
2009-02-20, by haftmann
reverted to old wellsorting algorithm
2009-02-20, by haftmann
fixed spurious proof failure
2009-02-20, by haftmann
consider changes variable names in theorem le_imp_power_dvd
2009-02-20, by haftmann
tuned and incremental version of wellsorting algorithm
2009-02-20, by haftmann
ignore sorts in bare types
2009-02-20, by haftmann
defensive implementation of pretty serialisation of lists and characters
2009-02-20, by haftmann
dropped Id
2009-02-20, by haftmann
experimental inclusion of new wellsorting algorithm for code equations
2009-02-20, by haftmann
merged
2009-02-20, by chaieb
merged
2009-02-17, by chaieb
merged
2009-02-17, by chaieb
fixed selection of premises
2009-02-17, by chaieb
cleaned up
2009-02-19, by huffman
declare of_int_number_of_eq [simp]
2009-02-19, by huffman
fix case_names
2009-02-19, by huffman
nicer induction/cases rules for numeral types
2009-02-19, by huffman
number_ring instances for numeral types
2009-02-19, by huffman
declare xor_compl_{left,right} [simp]
2009-02-19, by huffman
add rule for minus 1 at type bit
2009-02-19, by huffman
add formalization of a type of integers mod 2 to Library
2009-02-19, by huffman
new theory of real inner product spaces
2009-02-19, by huffman
add Powerdomain_ex.thy
2009-02-19, by huffman
add more ordering lemmas
2009-02-19, by huffman
avoid using ab_semigroup_idem_mult locale for powerdomains
2009-02-19, by huffman
merged
2009-02-19, by huffman
add header
2009-02-18, by huffman
move Polynomial.thy to Library
2009-02-18, by huffman
move FrechetDeriv.thy to Library
2009-02-18, by huffman
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-18, by huffman
half auto_solve default time out; increase manually in PG for large projects
2009-02-19, by kleing
merged
2009-02-18, by huffman
finish converting Deriv.thy to new polynomial library
2009-02-18, by huffman
generalize int_dvd_cancel_factor simproc to idom class
2009-02-18, by huffman
composition of polynomials
2009-02-18, by huffman
add some lemmas, cleaned up
2009-02-18, by huffman
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-02-18, by huffman
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
2009-02-18, by huffman
merged
2009-02-18, by huffman
more subsection headings
2009-02-18, by huffman
speed up proof of exp_exists
2009-02-18, by huffman
tuned
2009-02-18, by haftmann
sort instances wrt. to class hierarchy
2009-02-18, by haftmann
fixed signature
2009-02-18, by haftmann
tuned accessor name
2009-02-18, by haftmann
more precise improvement in instantiation user space type system
2009-02-18, by haftmann
do not drop arguments to 0, 1
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
reverted to previous version of Finite_Set.thy
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
merged
2009-02-18, by haftmann
first working version
2009-02-18, by haftmann
tuned comments, stripped ID, deleted superfluous code
2009-02-18, by haftmann
stripped ID
2009-02-18, by haftmann
Syntactic support for products over set intervals
2009-02-18, by paulson
No idea what happened here!
2009-02-18, by paulson
Even and odd powers of -1
2009-02-17, by paulson
merged
2009-02-18, by blanchet
Reintroduce set_interpreter for Collect and op :.
2009-02-17, by blanchet
Added Nitpick tag to 'of_int_of_nat'.
2009-02-16, by blanchet
add lemmas for exponentiation
2009-02-17, by huffman
merged
2009-02-17, by haftmann
unified variable names in case expressions; no exponential fork in translation of case expressions
2009-02-17, by haftmann
merged
2009-02-17, by huffman
remove redundant simp attributes for zdvd rules
2009-02-17, by huffman
lemmas abs_dvd_iff, dvd_abs_iff
2009-02-17, by huffman
Cleaned up IntDiv and removed subsumed lemmas.
2009-02-17, by nipkow
tune section headings; add square function
2009-02-16, by huffman
merged
2009-02-16, by huffman
rearrange subsections
2009-02-16, by huffman
remove instances num::semiring and num::linorder
2009-02-16, by huffman
datatype num = One | Dig0 num | Dig1 num
2009-02-16, by huffman
replace 1::num with One; remove monoid_mult instance
2009-02-16, by huffman
replace dec with double-and-decrement function
2009-02-15, by huffman
more default simp rules for sgn
2009-02-16, by haftmann
re-generated
2009-02-16, by haftmann
clarified import
2009-02-16, by haftmann
faster preprocessor
2009-02-16, by haftmann
added pdivmod on int (for code generation)
2009-02-16, by haftmann
merged
2009-02-16, by haftmann
tuned texts
2009-02-16, by haftmann
dropped Id
2009-02-16, by haftmann
dropped clause_suc_preproc for generic code generator
2009-02-16, by haftmann
new primrec
2009-02-16, by haftmann
Adapted to encoding of sets as predicates.
2009-02-16, by berghofe
enable auto-solve by default
2009-02-16, by kleing
merged
2009-02-16, by blanchet
Added nitpick attribute, and fixed typo.
2009-02-16, by blanchet
Added myself to testing list.
2009-02-16, by blanchet
dvd and setprod lemmas
2009-02-15, by nipkow
merged
2009-02-15, by nipkow
added finite_set_choice
2009-02-15, by nipkow
reject defined function in patterns with errmsg, e.g. f (f x) = x
2009-02-15, by krauss
fixed document
2009-02-15, by nipkow
more finiteness
2009-02-15, by nipkow
merged
2009-02-15, by nipkow
more finiteness
2009-02-15, by nipkow
merged
2009-02-14, by nipkow
more finiteness
2009-02-14, by nipkow
generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-14, by huffman
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-14, by huffman
add mult_delta lemmas; simplify some proofs
2009-02-14, by huffman
fix spelling
2009-02-14, by huffman
declare fps_nth as a typedef morphism; clean up instance proofs
2009-02-14, by huffman
add lemma surj_from_nat
2009-02-14, by huffman
fix document generation
2009-02-14, by huffman
merged
2009-02-14, by huffman
fix document generation
2009-02-14, by huffman
section -> subsection
2009-02-13, by huffman
add instance for cancel_comm_monoid_add
2009-02-13, by huffman
add class cancel_comm_monoid_add
2009-02-13, by huffman
more finiteness changes
2009-02-14, by nipkow
merged
2009-02-13, by nipkow
finiteness lemmas
2009-02-13, by nipkow
merged
2009-02-13, by huffman
unset execute bit
2009-02-13, by huffman
Tuned datatype antiquotation.
2009-02-13, by berghofe
made SMLNJ happy
2009-02-13, by haftmann
typo
2009-02-13, by kleing
find_consts: display the search criteria. (by Timothy Bourke)
2009-02-13, by kleing
find_consts: documentation. (by Timothy Bourke)
2009-02-13, by kleing
FindTheorems solves: update documentation (by Timothy Bourke)
2009-02-13, by kleing
fixed codegen tool
2009-02-13, by haftmann
merged
2009-02-13, by haftmann
fixed codegen tool
2009-02-13, by haftmann
merged
2009-02-13, by nipkow
Moved Nat_Int_Bij into Library
2009-02-13, by nipkow
removed Reflection session
2009-02-13, by haftmann
add lemma add_nonneg_eq_0_iff
2009-02-12, by huffman
add lemmas about sgn
2009-02-12, by huffman
added ML file for the find_consts command
2009-02-13, by kleing
added find_consts to NEWS and CONTRIBUTORS
2009-02-13, by kleing
New command find_consts searching for constants by type (by Timothy Bourke).
2009-02-13, by kleing
fix document generation
2009-02-12, by huffman
move countability proof from Rational to Countable; add instance rat :: countable
2009-02-12, by huffman
Moved FTA into Lib and cleaned it up a little.
2009-02-12, by nipkow
ordered_idom instance for polynomials
2009-02-11, by huffman
Export tactic interface for sizechange method
2009-02-11, by krauss
merged
2009-02-11, by haftmann
liberal inst_meet
2009-02-11, by haftmann
display code theorems with HOL equality
2009-02-11, by haftmann
merged
2009-02-11, by blanchet
Added serial_string to SAT solver input and output files, to prevent multithreading chaos.
2009-02-10, by blanchet
Added nitpick_const_simp attribute to recdef and record packages.
2009-02-10, by blanchet
Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.
2009-02-10, by blanchet
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
2009-02-10, by blanchet
Reintroduced nitpick_ind_intro attribute.
2009-02-09, by blanchet
merged
2009-02-09, by blanchet
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
2009-02-09, by blanchet
merged
2009-02-06, by blanchet
Merged.
2009-02-06, by blanchet
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
2009-02-06, by blanchet
fixed typo
2009-02-11, by kleing
updated NEWS etc with "solves" criterion and auto_solves
2009-02-11, by kleing
merged
2009-02-11, by nipkow
Moved Order_Relation into Library and moved some of it into Relation.
2009-02-11, by nipkow
Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-02-11, by kleing
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
2009-02-11, by kleing
const_name antiquotations
2009-02-10, by huffman
Repaired a proof that did, after all, refer to the theorem nat_induct2.
2009-02-10, by paulson
merged
2009-02-10, by paulson
Strengthened the induction rule nat_induct2.
2009-02-10, by paulson
Deleted the induction rule nat_induct2, which was too weak and not used even once.
2009-02-10, by paulson
merged
2009-02-09, by nipkow
fix to [arith]
2009-02-09, by nipkow
new attribute "arith" for facts supplied to arith.
2009-02-09, by nipkow
Nicer names in FindTheorems.
2009-02-09, by Timothy Bourke
added Determinants to Library
2009-02-09, by chaieb
Traces, Determinant of square matrices and some properties
2009-02-09, by chaieb
added Euclidean_Space and Glbs to Library
2009-02-09, by chaieb
fixed proof -- removed unnecessary sorry
2009-02-09, by chaieb
Fixed theorem reference
2009-02-09, by chaieb
(Real) Vectors in Euclidean space, and elementary linear algebra.
2009-02-09, by chaieb
A generic decision procedure for linear rea arithmetic and normed vector spaces
2009-02-09, by chaieb
Permutations, both general and specifically on finite sets.
2009-02-09, by chaieb
Imports Main in order to avoid the typerep problem
2009-02-09, by chaieb
A theory of greatest lower bounds
2009-02-09, by chaieb
Now imports Fact as suggested by Florian in order to avoid the typerep problem
2009-02-09, by chaieb
Added HOL/Library/Finite_Cartesian_Product.thy to Library
2009-02-09, by chaieb
A formalization of finite cartesian product types
2009-02-09, by chaieb
Proof method 'reify' is now reentrant.
2009-02-09, by hoelzl
added noatps
2009-02-08, by nipkow
check for destination directory, do not allocate it gratuitously
2009-02-07, by haftmann
Isar proof
2009-02-07, by haftmann
merged
2009-02-07, by haftmann
code theorems for nth, list_update
2009-02-07, by haftmann
added bulkload
2009-02-07, by haftmann
code theorems for nth, list_update
2009-02-07, by haftmann
added bulkload
2009-02-07, by haftmann
added Decision_Procs.thy
2009-02-07, by haftmann
merged
2009-02-06, by haftmann
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06, by haftmann
authentic syntax for List.nth
2009-02-06, by haftmann
Merged.
2009-02-06, by berghofe
Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
2009-02-06, by blanchet
Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-02-06, by chaieb
fixed import
2009-02-06, by chaieb
merged
2009-02-06, by haftmann
more robust failure in error situations
2009-02-06, by haftmann
mandatory prefix for index conversion operations
2009-02-06, by haftmann
added replace operation
2009-02-06, by haftmann
fixed dependencies : Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
2009-02-06, by chaieb
Updated NEWS about approximation
2009-02-05, by hoelzl
merged
2009-02-05, by haftmann
split of already properly working part of Quickcheck infrastructure
2009-02-05, by haftmann
code attribute applied before user attributes
2009-02-05, by haftmann
moved Random.thy to Library
2009-02-05, by haftmann
Add approximation method
2009-02-05, by hoelzl
Added new Float theory and moved old Library/Float.thy to ComputeFloat
2009-02-05, by hoelzl
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-02-05, by hoelzl
Make some Refute functions public so I can use them in Nitpick,
2009-02-04, by blanchet
merged
2009-02-04, by chaieb
Now catch ERROR exception thrown by find and friends
2009-02-04, by chaieb
dropped Id
2009-02-04, by haftmann
proper datatype abstraction example
2009-02-04, by haftmann
handling type classes without parameters
2009-02-03, by haftmann
adjusted theory name
2009-02-03, by haftmann
merged
2009-02-03, by haftmann
added stub about datatype abstraction
2009-02-03, by haftmann
changed name space policy for Haskell includes
2009-02-03, by haftmann
merged Big0
2009-02-03, by haftmann
added ROOT.ML for Reflection session
2009-02-03, by haftmann
merged
2009-02-03, by haftmann
established session HOL-Reflection
2009-02-03, by haftmann
established session HOL-Reflection
2009-02-03, by haftmann
regenerated presburger code
2009-02-03, by haftmann
merged Big0
2009-02-03, by haftmann
merge
2009-02-03, by nipkow
changed default timeout
2009-02-03, by immler
merged
2009-02-03, by haftmann
dropped global Nil/Append interpretation
2009-02-03, by haftmann
small fixes; removed Id
2009-02-03, by krauss
mergesort example: recdef->fun, localized
2009-02-03, by krauss
declare "nat o abs" as default measure for int
2009-02-03, by krauss
repaired accidental commit
2009-02-03, by haftmann
result for Swing.now;
2009-02-22, by wenzelm
replaced \overline by \vec;
2009-02-21, by wenzelm
updated generated files;
2009-02-21, by wenzelm
tuned;
2009-02-21, by wenzelm
updated generated files;
2009-02-20, by wenzelm
removed junk;
2009-02-20, by wenzelm
improved section "Rule composition";
2009-02-20, by wenzelm
tuned;
2009-02-20, by wenzelm
improved section on "Hereditary Harrop Formulae";
2009-02-20, by wenzelm
more on object-level rules;
2009-02-19, by wenzelm
updated generated files;
2009-02-18, by wenzelm
tuned;
2009-02-18, by wenzelm
more on local theories;
2009-02-18, by wenzelm
some text on local theory specifications;
2009-02-17, by wenzelm
some more Isar macros;
2009-02-17, by wenzelm
updated genereted files;
2009-02-16, by wenzelm
minor tuning and typographic fixes;
2009-02-16, by wenzelm
tuned refs;
2009-02-16, by wenzelm
removed rudiments of glossary;
2009-02-16, by wenzelm
removed rudiments of glossary;
2009-02-16, by wenzelm
removed unused glossary macros;
2009-02-16, by wenzelm
updated generated files;
2009-02-16, by wenzelm
observe usual theory naming conventions;
2009-02-16, by wenzelm
updated generated files;
2009-02-16, by wenzelm
tuned;
2009-02-16, by wenzelm
modernized some theory names;
2009-02-16, by wenzelm
eliminated old 'axclass';
2009-02-16, by wenzelm
avoid redefinition of FIXES/ASSUMES/SHOWS macros;
2009-02-16, by wenzelm
removed obsolete .cvsignore files;
2009-02-16, by wenzelm
removed obsolete axclass manual and examples;
2009-02-16, by wenzelm
explicit section for old/outdated manuals, which are still informative to some extent;
2009-02-15, by wenzelm
updated generated files;
2009-02-15, by wenzelm
added introduction;
2009-02-15, by wenzelm
added label;
2009-02-15, by wenzelm
removed obsolete section "User interfaces";
2009-02-15, by wenzelm
tuned spacing;
2009-02-15, by wenzelm
tuned;
2009-02-15, by wenzelm
updated generated files;
2009-02-15, by wenzelm
tuned;
2009-02-15, by wenzelm
added Isar/VM mode transition diagram;
2009-02-14, by wenzelm
replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted;
2009-02-14, by wenzelm
clean_string/clean_name: proper treatment of \<dash>;
2009-02-14, by wenzelm
misc tuning;
2009-02-13, by wenzelm
added section "Canonical reasoning patterns";
2009-02-12, by wenzelm
improved sorry/noproof markup;
2009-02-12, by wenzelm
tuned;
2009-02-12, by wenzelm
updated generated files;
2009-02-12, by wenzelm
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
2009-02-12, by wenzelm
more on Isar framework -- mostly from Trybulec Festschrift;
2009-02-11, by wenzelm
more refs;
2009-02-11, by wenzelm
some more Isar elements;
2009-02-11, by wenzelm
added "inference" entity;
2009-02-11, by wenzelm
some more macros;
2009-02-11, by wenzelm
proof/qed: optional methods;
2009-02-11, by wenzelm
tuned formal markup;
2009-02-11, by wenzelm
updated generated files;
2009-02-09, by wenzelm
added introductory examples;
2009-02-09, by wenzelm
set quick_and_dirty;
2009-02-09, by wenzelm
tuned chapter heading;
2009-02-09, by wenzelm
added parts;
2009-02-09, by wenzelm
updated generated files;
2009-02-09, by wenzelm
basic setup for chapter "The Isabelle/Isar Framework";
2009-02-09, by wenzelm
more refs;
2009-02-09, by wenzelm
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
2009-02-02, by wenzelm
export lexicographic_order_tac
2009-02-02, by krauss
fix potential incompleteness in SAT encoding
2009-02-02, by krauss
avoid name clash of generated modules and includes
2009-02-02, by haftmann
strict check for locale target
2009-02-02, by haftmann
fixed proposition slip
2009-02-02, by haftmann
added Mapping.thy to Library
2009-02-02, by haftmann
dropped Id
2009-02-02, by haftmann
updated type class section
2009-02-02, by haftmann
updated class documentation
2009-02-02, by haftmann
merged
2009-02-01, by haftmann
added State_Monad theory in session
2009-02-01, by haftmann
proper declared constants in class expressions
2009-02-01, by haftmann
merged
2009-01-31, by nipkow
added some simp rules
2009-01-31, by nipkow
fixed case
2009-01-30, by krauss
Fixed theory name
2009-01-30, by chaieb
Added Formal_Power_Series_Examples to HOL-ex image
2009-01-30, by chaieb
Some applications of formal power Series
2009-01-30, by chaieb
Added real related theorems from Fact.thy
2009-01-30, by chaieb
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
2009-01-30, by chaieb
moved upwards in thy graph, real related theorems moved to Transcendental.thy
2009-01-30, by chaieb
Enclosed name containing _'s in @{text ...} antiquotation to make document
2009-01-29, by berghofe
Added strong congruence rule for UN.
2009-01-29, by berghofe
Added abs_def attribute.
2009-01-29, by berghofe
removed definition of funpow , reusing that of Relation_Power
2009-01-29, by chaieb
Added Formal_Power_Series in imports
2009-01-29, by chaieb
A formalization of formal power series
2009-01-29, by chaieb
Inserted Formal_Power_Series.thy under Library
2009-01-29, by chaieb
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-29, by paulson
Minor reorganisation of the Skolemization code
2009-01-29, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-13, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-01-09, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-19, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-15, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-11, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-10, by paulson
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-10, by paulson
Updated comments.
2008-12-05, by paulson
dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-29, by chaieb
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
2009-01-28, by chaieb
merged
2009-01-29, by nipkow
commented out unused lemmas. May need to be put back by Brian.
2009-01-29, by nipkow
-
2009-01-28, by nipkow
removed spurious conflic msg
2009-01-28, by nipkow
merged
2009-01-28, by nipkow
merged - resolving conflics
2009-01-28, by nipkow
Replaced group_ and ring_simps by algebra_simps;
2009-01-28, by nipkow
merged
2009-01-28, by haftmann
explicit check for exactly one type variable in class specification elements
2009-01-28, by haftmann
merged
2009-01-28, by huffman
merged
2009-01-27, by huffman
removed use of prev_cont_thms reference
2009-01-22, by huffman
merged
2009-01-22, by huffman
add lemmas about div/mod with multiplication
2009-01-21, by huffman
add lemmas about smult
2009-01-21, by huffman
merged
2009-01-28, by haftmann
slightly adapted towards more uniformity with div/mod on nat
2009-01-28, by haftmann
merged
2009-01-28, by haftmann
Plain, Main form meeting points in import hierarchy
2009-01-28, by haftmann
Plain, Main form meeting points in import hierarchy
2009-01-28, by haftmann
added lemma abs_sng
2009-01-28, by haftmann
nat is a bot instance
2009-01-28, by haftmann
slightly adapted towards more uniformity with div/mod on nat
2009-01-28, by haftmann
Reflection.thy now in HOL/Library
2009-01-28, by haftmann
more robust treatment of SwingUtilities.isEventDispatchThread;
2009-01-28, by wenzelm
annotate shared vars as @volatile;
2009-01-28, by wenzelm
updated generated file;
2009-01-27, by wenzelm
added label;
2009-01-27, by wenzelm
plain non-dependent types;
2009-01-27, by wenzelm
turned IsarDocument into trait for IsabelleProcess;
2009-01-27, by wenzelm
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
2009-01-27, by wenzelm
thm_proof: recovered single-threaded version;
2009-01-27, by wenzelm
merged
2009-01-27, by wenzelm
recovered example types from WordMain.thy;
2009-01-27, by wenzelm
merged
2009-01-27, by wenzelm
added share_common_data -- reduces heap space, but takes long;
2009-01-27, by wenzelm
use https;
2009-01-27, by wenzelm
thm_proof: replaced lazy by composed futures;
2009-01-27, by wenzelm
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2009-01-27, by wenzelm
explicit constraints
2009-01-26, by haftmann
entry point for Word library now named Word
2009-01-26, by haftmann
fixed reading of class specs: declare class operations in context
2009-01-26, by haftmann
stripped Id
2009-01-26, by haftmann
streamlined definitions, executable equality
2009-01-26, by haftmann
tuned header
2009-01-26, by haftmann
entry point for Word library now named Word
2009-01-26, by haftmann
correct proof of assm_intro rule
2009-01-26, by haftmann
sorted_take, sorted_drop
2009-01-26, by haftmann
merged
2009-01-23, by haftmann
fixed fixme
2009-01-23, by haftmann
avoiding misleading name duplicate
2009-01-23, by haftmann
lemmas dom_const, dom_if
2009-01-23, by haftmann
merged
2009-01-23, by wenzelm
moved all output to watcher-thread
2009-01-23, by immler
be more liberal with selected code statements
2009-01-23, by haftmann
making SMLNJ happy
2009-01-23, by haftmann
tuned signature;
2009-01-22, by wenzelm
binding replaces Binding.T
2009-01-22, by haftmann
binding replaces bstring
2009-01-22, by haftmann
simplified handling of base sort, dropped axclass
2009-01-22, by haftmann
dropped print_interps
2009-01-22, by haftmann
binding replaces bstring
2009-01-22, by haftmann
merged
2009-01-21, by haftmann
allow empty class specs
2009-01-21, by haftmann
changed import hierarchy
2009-01-21, by haftmann
no base sort in class import
2009-01-21, by haftmann
updated generated files;
2009-01-21, by wenzelm
removed Ids;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
eliminated obsolete var morphism;
2009-01-21, by wenzelm
merged
2009-01-21, by wenzelm
tuned whitespace;
2009-01-21, by wenzelm
merged
2009-01-21, by wenzelm
removed vampire-wrapper (remote-script covers that)
2009-01-21, by immler
2 provers
2009-01-21, by immler
tuned;
2009-01-21, by immler
do not interrupt successful thread
2009-01-20, by immler
cancel whole group
2009-01-20, by immler
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
2009-01-20, by immler
pass timeout to prover;
2009-01-20, by immler
typo
2009-01-20, by immler
merged
2009-01-20, by immler
modified remote script;
2009-01-20, by immler
Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip
2009-01-19, by immler
removed useless
2009-01-14, by immler
simplified usage of remote-script; added compatible remote-atps
2009-01-12, by immler
dropped print_interps
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
merged
2009-01-21, by haftmann
merged
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
binding is alias for Binding.T
2009-01-21, by haftmann
dropped ID
2009-01-21, by haftmann
binding replaces bstring
2009-01-21, by haftmann
refined witness algebra
2009-01-21, by haftmann
code cleanup
2009-01-21, by haftmann
wrecked old locale package and related modules
2009-01-21, by haftmann
improved and corrected reading of class specs -- still draft version
2009-01-21, by haftmann
tuned
2009-01-21, by haftmann
tuned;
2009-01-20, by wenzelm
replaced java.util.Properties by plain association list;
2009-01-20, by wenzelm
replaced java.util.Properties by plain association list;
2009-01-20, by wenzelm
IsabelleSystem: provide Symbol.Interpretation;
2009-01-20, by wenzelm
more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
2009-01-20, by wenzelm
more robust handling of quick_and_dirty;
2009-01-19, by wenzelm
Merged, overriding earlier fix.
2009-01-19, by ballarin
Fixed tutorial to compile with new locales; grammar of new locale commands.
2009-01-19, by ballarin
removed Ids;
2009-01-19, by wenzelm
removed Ids;
2009-01-19, by wenzelm
intern names of elements and attributes;
2009-01-19, by wenzelm
merged
2009-01-19, by haftmann
lcp = paulson
2009-01-19, by haftmann
"code equation" replaces "defining equation"
2009-01-19, by haftmann
tuned
2009-01-19, by haftmann
improved tackling of subclasses
2009-01-19, by haftmann
tuned proof
2009-01-19, by haftmann
smart path detection
2009-01-18, by haftmann
corrected user aliases
2009-01-18, by haftmann
added churn script
2009-01-18, by haftmann
Scala wrapper for interactive Isar documents;
2009-01-18, by wenzelm
added append_list, encode_list;
2009-01-18, by wenzelm
join_results: when dependencies are resulved (but not finished yet),
2009-01-18, by wenzelm
with_attributes: make double sure that unsafe attributes are avoided;
2009-01-18, by wenzelm
bug fixes
2009-01-18, by nipkow
bug fixes
2009-01-18, by nipkow
improved calculation of morphisms and rules
2009-01-18, by haftmann
merged
2009-01-17, by haftmann
tuned signature
2009-01-17, by haftmann
exported depedencies; tuned signature
2009-01-17, by haftmann
merged
2009-01-17, by huffman
merged
2009-01-16, by huffman
use match_tac instead of resolve_tac for continuity simproc
2009-01-15, by huffman
more instance declarations for poly
2009-01-15, by huffman
add lemmas about degree
2009-01-15, by huffman
rename plength to psize
2009-01-15, by huffman
rename divmod_poly to pdivmod
2009-01-15, by huffman
merged.
2009-01-15, by huffman
add strictness and compactness lemmas to Product_Cpo.thy
2009-01-15, by huffman
rename Dsum.thy to Sum_Cpo.thy
2009-01-14, by huffman
minimize dependencies
2009-01-14, by huffman
add lemmas cont2monofunE, cont2cont_apply
2009-01-14, by huffman
add Product_Cpo.thy
2009-01-14, by huffman
change to simpler, more extensible continuity simproc
2009-01-14, by huffman
merged
2009-01-17, by nipkow
bug fix
2009-01-17, by nipkow
merged
2009-01-17, by haftmann
code cleanup
2009-01-17, by haftmann
explicit equation morphism
2009-01-17, by haftmann
close derivation of classrels
2009-01-17, by haftmann
no document for HOL-Base
2009-01-17, by haftmann
moved message markup into Scala layer -- reduced redundancy;
2009-01-16, by wenzelm
added parse_body_failsafe;
2009-01-16, by wenzelm
define_state: use empty_state;
2009-01-16, by wenzelm
provide end_document;
2009-01-16, by wenzelm
merged
2009-01-16, by wenzelm
run command: check theory name for init;
2009-01-16, by wenzelm
run_command: check theory name for init;
2009-01-16, by wenzelm
export check_name;
2009-01-16, by wenzelm
fixed location of Imperative_HOL
2009-01-16, by haftmann
adapted to changes in class package
2009-01-16, by haftmann
merged
2009-01-16, by haftmann
migrated class package to new locale implementation
2009-01-16, by haftmann
corrected preparation of instances: parameters are proper names, not raw terms
2009-01-16, by haftmann
migrated class package to new locale implementation
2009-01-16, by haftmann
merged
2009-01-16, by wenzelm
fold_entries: non-optional start, permissive;
2009-01-16, by wenzelm
Result.toString: XML output of status messages;
2009-01-15, by wenzelm
added HOL-Base image
2009-01-16, by haftmann
moved Univ_Poly to Library
2009-01-16, by haftmann
merged
2009-01-16, by haftmann
tuned
2009-01-16, by haftmann
added cert_read_declaration; more exports; tuned signature
2009-01-16, by haftmann
merged
2009-01-15, by wenzelm
command 'Isar.edit_document': actually invoke edit_document;
2009-01-15, by wenzelm
merged
2009-01-15, by haftmann
fixed error message spacing
2009-01-15, by haftmann
tuned interpretation code
2009-01-15, by haftmann
tuned
2009-01-15, by haftmann
type constraints and sort intersection
2009-01-15, by haftmann
dropped $Id$
2009-01-15, by haftmann
decativate Toplevel.debug after reading
2009-01-15, by haftmann
exported break reference
2009-01-15, by Christian Urban
tuned;
2009-01-15, by wenzelm
edit_document: proper edits/edit markup, including the document id;
2009-01-15, by wenzelm
replaced command_state by edits/edit;
2009-01-15, by wenzelm
removed junk;
2009-01-15, by wenzelm
merged
2009-01-15, by wenzelm
one more [code del] declaration
2009-01-14, by huffman
misc cleanup and simplification;
2009-01-15, by wenzelm
added run_command (from isar_document.ML);
2009-01-15, by wenzelm
added command_state markup;
2009-01-15, by wenzelm
tuned ASCII art;
2009-01-14, by wenzelm
declare pCons_0_0 [code post]
2009-01-13, by huffman
merged
2009-01-13, by huffman
code generation for polynomials
2009-01-13, by huffman
merged
2009-01-13, by wenzelm
more [code del] declarations
2009-01-13, by huffman
declare more definitions [code del]
2009-01-13, by huffman
define polynomial multiplication using poly_rec
2009-01-13, by huffman
merged.
2009-01-13, by huffman
declare smult rules [simp]
2009-01-13, by huffman
simplify proof of coeff_mult_degree_sum
2009-01-13, by huffman
convert Deriv.thy to use new Polynomial library (incomplete)
2009-01-13, by huffman
Integration imports ATP_Linkup (for metis)
2009-01-13, by huffman
misc internal rearrangements;
2009-01-13, by wenzelm
replaced sys_error by plain error;
2009-01-13, by wenzelm
merged
2009-01-13, by wenzelm
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
2009-01-12, by huffman
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
2009-01-12, by huffman
add Polynomial.thy to makefile
2009-01-12, by huffman
add lemmas poly_power, poly_roots_finite
2009-01-12, by huffman
declare dvd_minus_iff and minus_dvd_iff [iff]
2009-01-12, by huffman
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
2009-01-12, by huffman
added Isar/isar_document.ML: Interactive Isar documents.
2009-01-13, by wenzelm
export list;
2009-01-13, by wenzelm
correctness and uniqueness of synthetic division
2009-01-12, by huffman
add synthetic division algorithm for polynomials
2009-01-12, by huffman
add list-style syntax for pCons
2009-01-12, by huffman
add recursion combinator poly_rec; define poly function using poly_rec
2009-01-12, by huffman
add lemmas degree_{add,diff}_less
2009-01-12, by huffman
merged
2009-01-11, by wenzelm
new theory of polynomials
2009-01-11, by huffman
tuned categories;
2009-01-11, by wenzelm
added outer_keyword.scala: Isar command keyword classification;
2009-01-11, by wenzelm
added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-11, by wenzelm
load main entry points sequentially, for reduced memory demands;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
merged
2009-01-11, by wenzelm
merged
2009-01-11, by haftmann
explicit bookkeeping of intro rules and axiom
2009-01-11, by haftmann
stripped Id
2009-01-11, by haftmann
construct explicit class morphism
2009-01-11, by haftmann
less ambitious ML_OPTIONS;
2009-01-11, by wenzelm
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10, by wenzelm
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10, by wenzelm
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10, by wenzelm
remove_thy: perform PureThy.cancel_proofs;
2009-01-10, by wenzelm
added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10, by wenzelm
added pending_groups -- accumulates task groups of local derivations only;
2009-01-10, by wenzelm
added cancel_group;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10, by wenzelm
load_thy: explicit after_load phase for presentation;
2009-01-10, by wenzelm
excursion: commit_exit internally -- checkpoints are fully persistent now;
2009-01-10, by wenzelm
slightly more robust matching of session name;
2009-01-10, by wenzelm
merged
2009-01-10, by wenzelm
fixed proof involving dvd;
2009-01-10, by wenzelm
tuned;
2009-01-10, by wenzelm
added force_result;
2009-01-10, by wenzelm
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2009-01-10, by wenzelm
simplified join_proofs;
2009-01-10, by wenzelm
merged
2009-01-09, by wenzelm
added split_thy_path;
2009-01-09, by wenzelm
added running task markup;
2009-01-09, by wenzelm
tuned;
2009-01-08, by wenzelm
merged
2009-01-08, by wenzelm
merged
2009-01-09, by wenzelm
merged.
2009-01-09, by huffman
fix proof broken by changes in dvd theory
2009-01-09, by huffman
merged.
2009-01-08, by huffman
remove type-specific proofs
2009-01-08, by huffman
add lemma dvd_diff to class comm_ring_1
2009-01-08, by huffman
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
2009-01-08, by huffman
move lemmas mult_minus{left,right} inside class ring
2009-01-08, by huffman
clean up division_ring proofs
2009-01-08, by huffman
add class ring_div; generalize mod/diff/minus proofs for class ring_div
2009-01-08, by huffman
generalize zmod_zmod_cancel -> mod_mod_cancel
2009-01-08, by huffman
generalize some div/mod lemmas; remove type-specific proofs
2009-01-08, by huffman
add tracing for domain package proofs
2009-01-07, by huffman
rename abbreviation square -> power2, to match theorem names
2009-01-06, by huffman
merged
2009-01-09, by haftmann
split of Imperative_HOL theories from HOL-Library
2009-01-08, by haftmann
NEWS and CONTRIBUTORS
2009-01-08, by haftmann
dded code_thm antiquotation
2009-01-08, by haftmann
made SML/NJ happy
2009-01-08, by haftmann
merged
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
tuned siganture of locale.ML
2009-01-07, by haftmann
tuned signature; internal code reorganisation
2009-01-07, by haftmann
tuned signature; changed locale predicate name convention
2009-01-07, by haftmann
changed locale predicate name convention
2009-01-07, by haftmann
inductive: added fork_mono flag;
2009-01-07, by wenzelm
added fork_mono flag, which is usually enabled in batch-mode only;
2009-01-07, by wenzelm
Proof.global_future_terminal_proof;
2009-01-07, by wenzelm
Proof.global_future_proof;
2009-01-07, by wenzelm
future_proof: refined version covers local_future_proof and global_future_proof;
2009-01-07, by wenzelm
more robust propagation of errors through bulk jobs;
2009-01-07, by wenzelm
qed/after_qed: singleton result;
2009-01-07, by wenzelm
Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;
2009-01-07, by wenzelm
future_terminal_proof: no fork for interactive mode, assert_backward;
2009-01-07, by wenzelm
added local_theory';
2009-01-07, by wenzelm
merged
2009-01-07, by haftmann
proper local_theory after Class.class
2009-01-07, by haftmann
more parallel loading;
2009-01-06, by wenzelm
more parallel loading;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
merged.
2009-01-06, by huffman
make cont_proc handle eta-contracted terms
2009-01-06, by huffman
implement is_closed_term using Term.loose_bvar
2009-01-06, by huffman
use Thm.close_derivation instead of standard
2009-01-05, by huffman
tuned;
2009-01-06, by wenzelm
merged
2009-01-06, by wenzelm
renamed structure ParList to Par_List;
2009-01-06, by wenzelm
parallelized merge_data;
2009-01-06, by wenzelm
tuned map: reduced overhead due to bulk jobs;
2009-01-06, by wenzelm
added is_valid;
2009-01-06, by wenzelm
future_terminal_proof: check Future.enabled;
2009-01-06, by wenzelm
merged
2009-01-06, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-06, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-05, by haftmann
locale -> old_locale, new_locale -> locale
2009-01-05, by haftmann
removed locale adaption layer
2009-01-05, by haftmann
rearranged target theories
2009-01-05, by haftmann
removed locale adaption layer
2009-01-05, by haftmann
merged
2009-01-05, by wenzelm
misc tuning and modernization;
2009-01-05, by wenzelm
merged.
2009-01-05, by huffman
add lemma psize_unique; simplify some proofs
2008-12-29, by huffman
minimize imports
2008-12-29, by huffman
parallelize some internal proofs via Proof.future_terminal_proof;
2009-01-05, by wenzelm
added future_terminal_proof;
2009-01-05, by wenzelm
Isar.init;
2009-01-05, by wenzelm
simplified tty model -- back to plain list history, which is independent of editor model;
2009-01-05, by wenzelm
added is_control, is_regular, is_theory_begin;
2009-01-05, by wenzelm
more precise is_relevant: requires original main goal, not initial goal state;
2009-01-04, by wenzelm
tuned protect, conclude: Drule.comp_no_flatten;
2009-01-04, by wenzelm
added comp_no_flatten;
2009-01-04, by wenzelm
future proofs: back to Future.fork_pri ~1 for improved parallelism;
2009-01-04, by wenzelm
cancel: unique threads;
2009-01-04, by wenzelm
more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;
2009-01-03, by wenzelm
added eq_group;
2009-01-03, by wenzelm
merged
2009-01-03, by haftmann
separator, is_qualified
2009-01-03, by haftmann
added instance for bot, top
2009-01-03, by haftmann
added binding.ML
2009-01-03, by haftmann
merged
2009-01-02, by haftmann
merged
2009-01-02, by haftmann
improved boostrap order: theory_target.ML before expression.ML
2009-01-02, by haftmann
named code theorem for Fract_norm
2009-01-02, by haftmann
tuned settings;
2009-01-02, by wenzelm
merged
2009-01-02, by wenzelm
removed references to OldTerm.*
2009-01-02, by krauss
tuned message_text;
2009-01-02, by wenzelm
removed obsolete XML mode;
2009-01-02, by wenzelm
xsymbols: use plain Symbol.output;
2009-01-02, by wenzelm
Markup.no_output;
2009-01-02, by wenzelm
added output;
2009-01-02, by wenzelm
removed unused add_substring;
2009-01-02, by wenzelm
renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
2009-01-02, by wenzelm
removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
2009-01-02, by wenzelm
updated rendering of inner token markup;
2009-01-02, by wenzelm
more detailed inner token markup;
2009-01-02, by wenzelm
added numeral, which supercedes num, xnum, float;
2009-01-02, by wenzelm
renamed token markup "_xstr" to "_inner_string";
2009-01-02, by wenzelm
removed dead code;
2009-01-02, by wenzelm
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
2009-01-02, by wenzelm
tuned;
2009-01-02, by wenzelm
Isar.command: plain Position.id;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added type 'a parser, simplified signature;
2009-01-02, by wenzelm
added props_text (from outer_parse.ML);
2009-01-02, by wenzelm
added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
2009-01-02, by wenzelm
added id;
2009-01-02, by wenzelm
MetaSimplifier.SIMPLIFIER;
2009-01-02, by wenzelm
fixed assumption proof;
2009-01-02, by wenzelm
tuned header and description of boot files;
2009-01-02, by wenzelm
merged;
2009-01-01, by wenzelm
normalized some ML type/val aliases;
2009-01-01, by wenzelm
assumption/close: discontinued implicit prems;
2009-01-01, by wenzelm
avoid implicit use of prems;
2009-01-01, by wenzelm
updated generated files;
2009-01-01, by wenzelm
eliminated implicit use of prems;
2009-01-01, by wenzelm
updated generated files;
2009-01-01, by wenzelm
updated type 'a lazy;
2009-01-01, by wenzelm
proper import of ~~/src/HOL/ex/ReflectedFerrack;
2009-01-01, by wenzelm
crude adaption to intermediate class/locale version;
2009-01-01, by wenzelm
crude adaption to new locales;
2009-01-01, by wenzelm
avoid implicit prems -- tuned proofs;
2009-01-01, by wenzelm
avoid implicit use of prems;
2009-01-01, by wenzelm
Term.add_consts;
2009-01-01, by wenzelm
eliminated OldTerm.(add_)term_consts;
2009-01-01, by wenzelm
avoid polymorphic equality;
2009-01-01, by wenzelm
eliminated OldTerm.(add_)term_consts;
2009-01-01, by wenzelm
added canonical add_const_names, add_consts;
2009-01-01, by wenzelm
provide structure CharVector;
2009-01-01, by wenzelm
isabelle-process;
2009-01-01, by wenzelm
updated sessions;
2009-01-01, by wenzelm
removed unused add_term_free_names;
2008-12-31, by wenzelm
eliminated OldTerm.add_term_free_names;
2008-12-31, by wenzelm
updated header;
2008-12-31, by wenzelm
Term.declare_typ_names, Term.declare_term_frees;
2008-12-31, by wenzelm
added declare_term_frees;
2008-12-31, by wenzelm
Term.declare_term_frees;
2008-12-31, by wenzelm
qualified Term.rename_wrt_term;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
use fold_aterms directly;
2008-12-31, by wenzelm
use exists_Const directly;
2008-12-31, by wenzelm
use regular Term.add_XXX etc.;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31, by wenzelm
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-31, by wenzelm
use exists_subterm directly;
2008-12-31, by wenzelm
use exists_subterm directly;
2008-12-31, by wenzelm
use regular Term.add_vars, Term.add_frees etc.;
2008-12-31, by wenzelm
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-31, by wenzelm
use regular Term.add_vars, Term.add_frees etc.;
2008-12-31, by wenzelm
added old_term.ML;
2008-12-31, by wenzelm
Some old-style term operations.
2008-12-31, by wenzelm
freeze_thaw: canonical Term.add_XXX operations;
2008-12-30, by wenzelm
varify: regular name context;
2008-12-30, by wenzelm
canonical Term.add_var_names, Term.add_tvar_namesT;
2008-12-30, by wenzelm
canonical Term.add_var_names;
2008-12-30, by wenzelm
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
2008-12-30, by wenzelm
removed unused head_name_of;
2008-12-30, by wenzelm
merged
2008-12-30, by wenzelm
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
2008-12-30, by wenzelm
New locales.
2008-12-30, by ballarin
Merged.
2008-12-30, by ballarin
Temporarily avoid type errors in parse phase.
2008-12-30, by ballarin
More liberal consistency check for defines elements.
2008-12-23, by ballarin
All logics ported to new locales.
2008-12-19, by ballarin
Merged.
2008-12-19, by ballarin
adapted statespace module to new locales;
2008-12-18, by Norbert Schirmer
More porting to new locales.
2008-12-19, by ballarin
Intro_locales_tac knows about defines elements; more robust export morphism.
2008-12-19, by ballarin
More porting to new locales.
2008-12-19, by ballarin
Merged.
2008-12-19, by ballarin
More porting to new locales
2008-12-19, by ballarin
Merged.
2008-12-18, by ballarin
More porting to new locales.
2008-12-17, by ballarin
Prevent defines from being checked in interpretation.
2008-12-17, by ballarin
Merged.
2008-12-16, by ballarin
More porting to new locales.
2008-12-16, by ballarin
Merged.
2008-12-16, by ballarin
More porting to new locales.
2008-12-16, by ballarin
More porting to new locales.
2008-12-15, by ballarin
Ported HOL and HOL-Library to new locales.
2008-12-14, by ballarin
Fixed legacy locale keywords (went to ZF rather than default keywords file).
2008-12-14, by ballarin
Merged.
2008-12-14, by ballarin
Merged.
2008-12-12, by ballarin
Porting to new locales.
2008-12-12, by ballarin
Theory target distinguishes old and new locales.
2008-12-12, by ballarin
Merged.
2008-12-12, by ballarin
Ported to new locales.
2008-12-12, by ballarin
Merged; updated interpretation command in isar_syn.ML.
2008-12-12, by ballarin
Merged.
2008-12-11, by ballarin
Conversion of HOL-Main and ZF to new locales.
2008-12-11, by ballarin
Add inherited registrations.
2008-12-19, by ballarin
Refactored: evaluate specification text only in locale declarations.
2008-12-18, by ballarin
Transfer theorems in print_locale.
2008-12-17, by ballarin
Attributes not applied in foundational version of fact.
2008-12-17, by ballarin
Transfer morphism with theory closure.
2008-12-16, by ballarin
Finer-grained activation so that facts from earlier elements are available.
2008-12-16, by ballarin
Transfer theorems before activation.
2008-12-16, by ballarin
Use correct mode when parsing elements and conclusion.
2008-12-16, by ballarin
Strict prefixes in locales expressions.
2008-12-14, by ballarin
Propagate theorems to registrations.
2008-12-12, by ballarin
Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2008-12-12, by ballarin
Equations in interpretation as goals.
2008-12-12, by ballarin
Interpretation in theories: first version with equations.
2008-12-11, by ballarin
Clarified comment.
2008-12-11, by ballarin
Use prefix component of bindings for locale prefixes.
2008-12-10, by ballarin
Missing dependency
2008-12-10, by ballarin
Preserve idents (expression in sublocale).
2008-12-10, by ballarin
added POSITION_PROPERTIES;
2008-12-29, by wenzelm
tuned;
2008-12-29, by wenzelm
override toString method;
2008-12-29, by wenzelm
Swing utilities.
2008-12-29, by wenzelm
merged
2008-12-29, by wenzelm
optional exception logging;
2008-12-29, by wenzelm
merged
2008-12-29, by haftmann
pretty printer for bindings
2008-12-29, by haftmann
adapted HOL source structure to distribution layout
2008-12-29, by haftmann
tuned;
2008-12-29, by wenzelm
more markup elements;
2008-12-29, by wenzelm
tuned;
2008-12-29, by wenzelm
merged
2008-12-29, by wenzelm
explicit EventBus for results;
2008-12-29, by wenzelm
added methods "+" and "-";
2008-12-29, by wenzelm
Generic event bus.
2008-12-29, by wenzelm
eliminated fun/val confusion
2008-12-29, by haftmann
merged
2008-12-28, by huffman
clean up proofs of lemma Maclaurin
2008-12-28, by huffman
disabled old jedit plugin;
2008-12-28, by wenzelm
more markup elements;
2008-12-28, by wenzelm
more markup elements;
2008-12-28, by wenzelm
removed duplicate sum_case used only by function package;
2008-12-27, by krauss
tuned NEWS; CONTRIBUTORS
2008-12-27, by krauss
renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-27, by krauss
tuned;
2008-12-27, by wenzelm
merged
2008-12-27, by wenzelm
refined execute, which replaces exec/exec2;
2008-12-27, by wenzelm
maintain initial process environment;
2008-12-27, by wenzelm
merged
2008-12-27, by haftmann
tackling simultaneous val/fun bindings
2008-12-27, by haftmann
proper class IsabelleSystem -- no longer static;
2008-12-27, by wenzelm
PATH: /opt/local/bin is back again (required for latex etc.);
2008-12-27, by wenzelm
merged.
2008-12-24, by huffman
clean up lemmas about ln
2008-12-24, by huffman
clean up lemmas about exp
2008-12-24, by huffman
more proofs about differentiable
2008-12-24, by huffman
use less_iff_Suc_add instead of less_add_one
2008-12-24, by huffman
rearranged subsections; cleaned up some proofs
2008-12-24, by huffman
move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-24, by huffman
cleaned up some proofs; removed redundant simp rules
2008-12-24, by huffman
move sin and cos to their own subsection
2008-12-23, by huffman
clean up some proofs; remove unused lemmas
2008-12-23, by huffman
tuned;
2008-12-23, by wenzelm
* Proofs of are run in parallel on multi-core systems;
2008-12-23, by wenzelm
updated generated file;
2008-12-23, by wenzelm
updated thread-safe programming;
2008-12-23, by wenzelm
updated generated file;
2008-12-23, by wenzelm
added float_token, and num_const, float_const;
2008-12-23, by wenzelm
renamed terminal category "float" to "float_token", to avoid name
2008-12-23, by wenzelm
manual file type setup using AppHack 1.1;
2008-12-23, by wenzelm
target PWD;
2008-12-23, by wenzelm
updated scala path;
2008-12-23, by wenzelm
added platform_file;
2008-12-23, by wenzelm
proper -X option;
2008-12-22, by wenzelm
unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
2008-12-22, by wenzelm
more sophisticated MacOS interface script (mostly for Carbon Emacs);
2008-12-22, by wenzelm
updated web style for Mercurial 1.1.1;
2008-12-21, by wenzelm
misc webstyle adaptions;
2008-12-21, by wenzelm
updated web style for Mercurial 1.1;
2008-12-20, by wenzelm
removed Ids;
2008-12-20, by wenzelm
merged
2008-12-20, by wenzelm
removed Ids;
2008-12-20, by wenzelm
merged.
2008-12-19, by huffman
constdefs -> definition
2008-12-18, by huffman
removed Ids;
2008-12-19, by wenzelm
merged.
2008-12-18, by huffman
remove cvs Id tags
2008-12-16, by huffman
merged
2008-12-17, by wenzelm
basic setup for MacOS application bundle;
2008-12-17, by wenzelm
GHC ext pragma in generated Haskell modules
2008-12-17, by haftmann
dropped Ids
2008-12-17, by haftmann
temporary adaption to new locale code
2008-12-17, by haftmann
restructured; circumvent sort problem
2008-12-17, by haftmann
merged.
2008-12-16, by huffman
new theory Dsum: cpo of disjoint sum
2008-12-16, by huffman
scale dependency graph in document
2008-12-16, by huffman
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-16, by Christian Urban
proper document antiquotations;
2008-12-16, by wenzelm
merged
2008-12-16, by wenzelm
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-16, by krauss
future proofs: Future.fork_pri 1 minimizes queue length and pending promises
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
Future.fork_pri;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
removed old scheduler;
2008-12-16, by wenzelm
tuned enqueue: plain add_edge, acyclic not required here;
2008-12-16, by wenzelm
tuned messages;
2008-12-15, by wenzelm
updated generated file;
2008-12-15, by wenzelm
repaired railroad accident;
2008-12-15, by wenzelm
updated generated files;
2008-12-15, by wenzelm
added 'atp_messages' command, which displays recent messages synchronously;
2008-12-15, by wenzelm
merged
2008-12-15, by nipkow
flipped fold implementation
2008-12-15, by nipkow
merged
2008-12-11, by nipkow
codegen
2008-12-11, by nipkow
code for {x:A. P(x)} and for fold
2008-12-11, by nipkow
Testfile for Stefan's code generator
2008-12-11, by nipkow
moved value.ML to src/Tools
2008-12-15, by haftmann
\underscoreoff is now default
2008-12-15, by haftmann
tuned some proofs
2008-12-15, by Christian Urban
removed Ids;
2008-12-13, by wenzelm
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
Unified syntax of nominal_primrec with the one used by fun(ction) and new
2008-12-13, by berghofe
Modified nominal_primrec to make it work with local theories, unified syntax
2008-12-13, by berghofe
merged
2008-12-13, by wenzelm
tuned comments;
2008-12-13, by wenzelm
tuned ML_OPTIONS for improved multicore performance;
2008-12-13, by wenzelm
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
2008-12-13, by wenzelm
requires: check ancestors directly;
2008-12-13, by wenzelm
Context.display_names;
2008-12-13, by wenzelm
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
2008-12-12, by wenzelm
usage: echo ML settings as well;
2008-12-13, by wenzelm
future proofs: more robust check via Future.enabled;
2008-12-12, by wenzelm
removed former Isabelle font (cf. IsabelleItalic);
2008-12-11, by wenzelm
incorporated isabelle-fonts side-branch (forced merge);
2008-12-11, by wenzelm
replaced single quote by mathematical prime;
2008-09-06, by wenzelm
generated file;
2008-08-24, by wenzelm
bold version: math glyphs from plain IsabelleMono;
2008-08-24, by wenzelm
fixed rangle;
2008-08-24, by wenzelm
use dash from text font, not math;
2008-08-24, by wenzelm
added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
2008-08-24, by wenzelm
generated ttf;
2008-08-22, by wenzelm
renamed to IsabelleMono;
2008-08-22, by wenzelm
added README with original licenses;
2008-08-22, by wenzelm
renamed Isabelle to IsabelleItalic;
2008-08-22, by wenzelm
fixed rangle glyph;
2008-08-22, by wenzelm
the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
2008-08-22, by wenzelm
Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
2008-08-22, by wenzelm
Isabelle font, based on TeX glyhps;
2008-08-22, by wenzelm
enable future_scheduler by default;
2008-12-11, by wenzelm
ISABELLE_USEDIR_OPTIONS: -M max is default;
2008-12-11, by wenzelm
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
2008-12-11, by wenzelm
removed spurious exception_trace;
2008-12-11, by wenzelm
print_theorems: more robust difference, even after finished proof;
2008-12-11, by wenzelm
export context_node;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
more antiquotations;
2008-12-10, by wenzelm
pcpodef package: state two goals, instead of encoded conjunction;
2008-12-11, by wenzelm
recovered goal_pat;
2008-12-11, by wenzelm
inhabitance goal is now stated in original form and result contracted --
2008-12-11, by wenzelm
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
2008-12-11, by wenzelm
add_typedef: unfold set_def in tactical proof as well;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
Theory.checkpoint before commencing proof;
2008-12-11, by wenzelm
misc tuning and modernisation;
2008-12-11, by wenzelm
merged
2008-12-10, by wenzelm
logically separate typedef axiomatization from constant definition
2008-12-08, by krauss
add def before setting up goal
2008-12-08, by krauss
killed dead code
2008-12-07, by krauss
constrain type inference to sort "type"
2008-12-11, by krauss
merged.
2008-12-10, by huffman
cleaned up some proofs in Cfun.thy
2008-12-10, by huffman
implement cont_proc theorem cache using theory data
2008-12-10, by huffman
use ML antiquotations
2008-12-10, by huffman
clean up diff_bin_simps
2008-12-10, by huffman
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
2008-12-10, by huffman
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
requires RComplete;
2008-12-10, by wenzelm
merged.
2008-12-10, by huffman
move all neg-related lemmas to NatBin; make type of neg specific to int
2008-12-09, by huffman
separate neg_simps from rel_simps
2008-12-09, by huffman
use {less,le}_number_of in integer simprocs
2008-12-09, by huffman
use lemma lists defined in Int.thy
2008-12-09, by huffman
Merged.
2008-12-10, by ballarin
Satisfy a_axioms.
2008-12-10, by ballarin
Merged.
2008-12-10, by ballarin
Enable keyword 'structure' in for clause of locale expression.
2008-12-10, by ballarin
Correct order of defines in specification.
2008-12-09, by ballarin
Pass on defines in inheritance; reject illicit defines created by instantiation.
2008-12-09, by ballarin
Order of implicit parameters in locale expression.
2008-12-09, by ballarin
NewLocale.intro_locales_tac added to Class.default_intro_tac.
2008-12-09, by ballarin
When adding locales, delay notes until local theory is built.
2008-12-09, by ballarin
merged
2008-12-10, by nipkow
moved ContNotDenum into Library
2008-12-10, by nipkow
move lemmas from Numeral_Type.thy to other theories
2008-12-09, by huffman
instantiation option :: (enum) enum
2008-12-09, by huffman
instance inat :: semiring_char_0
2008-12-09, by huffman
Default names for definitions.
2008-12-08, by ballarin
Proper shape of assumptions generated from Defines elements.
2008-12-08, by ballarin
Merged.
2008-12-08, by ballarin
Explicitly close up defines.
2008-12-08, by ballarin
Interpretation in proof contexts.
2008-12-05, by ballarin
tuned LaTeX files
2008-12-08, by haftmann
tuned LaTeX files
2008-12-08, by haftmann
merged.
2008-12-06, by huffman
multiplication for type inat
2008-12-06, by huffman
fix proofs
2008-12-06, by huffman
change lemmas to avoid using neg
2008-12-06, by huffman
simplify less_nat_number_of
2008-12-05, by huffman
add lemma le_nat_number_of
2008-12-05, by huffman
merged
2008-12-06, by wenzelm
adapted to changes in binding module
2008-12-06, by haftmann
merged
2008-12-06, by haftmann
Name.name_of -> Binding.base_name
2008-12-05, by haftmann
corrected theory path
2008-12-05, by haftmann
removed Table.extend, NameSpace.extend_table
2008-12-05, by haftmann
renamed force_proof to join_proof;
2008-12-06, by wenzelm
renamed force_proofs to join_proofs;
2008-12-06, by wenzelm
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
2008-12-06, by wenzelm
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
2008-12-06, by wenzelm
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
2008-12-06, by wenzelm
added new_task;
2008-12-06, by wenzelm
added constant value;
2008-12-06, by wenzelm
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
2008-12-05, by wenzelm
uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
2008-12-05, by wenzelm
Merged.
2008-12-05, by ballarin
Interpretation in theories including interaction with subclass relation.
2008-12-05, by ballarin
merged
2008-12-05, by haftmann
dropped NameSpace.declare_base
2008-12-05, by haftmann
fix proofs
2008-12-04, by huffman
merged.
2008-12-04, by huffman
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
2008-12-04, by huffman
remove duplicated lemmas
2008-12-04, by huffman
include iszero_simps in lemmas comp_arith
2008-12-04, by huffman
add named lemma lists: neg_simps and iszero_simps
2008-12-04, by huffman
change arith_special simps to avoid using neg
2008-12-04, by huffman
merged
2008-12-05, by kleing
run test for sunbroy2 on /tmp,
2008-12-05, by kleing
merged
2008-12-05, by wenzelm
refined Future.fork interfaces, no longer export Future.future;
2008-12-04, by wenzelm
fork/map: no inheritance of group (structure is nested, not parallel);
2008-12-04, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
future_scheduler: no global task group, exceptions via collective join;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
2008-12-04, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
2008-12-04, by wenzelm
renamed type Future.T to future;
2008-12-04, by wenzelm
renamed type Lazy.T to lazy;
2008-12-04, by wenzelm
merged.
2008-12-04, by huffman
change more lemmas to avoid using iszero
2008-12-04, by huffman
change some lemmas to avoid using iszero
2008-12-03, by huffman
enable eq_bin_simps for simplifying equalities on numerals
2008-12-03, by huffman
merged
2008-12-04, by haftmann
cleaned up binding module and related code
2008-12-04, by haftmann
NEWS
2008-12-04, by nipkow
fix proofs related to simplification of inequalities on numerals
2008-12-03, by huffman
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
2008-12-03, by huffman
simplify proof of less_nat_number_of
2008-12-03, by huffman
merged.
2008-12-03, by huffman
fixed proofs due to changes in Int.thy
2008-12-03, by huffman
cleaned up subsection headings;
2008-12-03, by huffman
sources are not executable;
2008-12-03, by wenzelm
eliminated traces of old Distribution directory;
2008-12-03, by wenzelm
merged
2008-12-03, by wenzelm
remove *.lof as well;
2008-12-03, by wenzelm
merged
2008-12-03, by haftmann
made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-12-03, by haftmann
Sublocale: removed public after_qed; identifiers private to NewLocale.
2008-12-03, by ballarin
Made global_note_qualified public.
2008-12-03, by ballarin
more examples
2008-12-03, by webertj
fixed typo
2008-12-03, by haftmann
unfold_locales is default method - no need for explicit references
2008-12-03, by haftmann
Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle
2008-12-02, by wenzelm
Corrected imports.
2008-12-02, by berghofe
clean up imports related to ContNotDenum
2008-12-01, by huffman
ignore aux stuff in doc-src;
2008-12-01, by wenzelm
merged
2008-12-01, by haftmann
new Binding module
2008-12-01, by haftmann
Locale.*note* with conventional argument type
2008-12-01, by haftmann
added code equation for subset
2008-12-01, by haftmann
Merged again.
2008-12-01, by ballarin
Merged.
2008-12-01, by ballarin
No resolution of patterns within context statements.
2008-12-01, by ballarin
removed CVS Id;
2008-12-02, by wenzelm
proper check of ISABELLE_TOOLS directories;
2008-12-01, by wenzelm
removed obsolete tags (leftover from old CVS branches);
2008-12-01, by wenzelm
makedist -- make Isabelle source distribution (Mercurial version);
2008-12-01, by wenzelm
renamed makedist_mercurial to makedist, deleting the old version;
2008-12-01, by wenzelm
updated to python2.5;
2008-12-01, by wenzelm
convert to isabelle-cvs, the old version;
2008-12-01, by wenzelm
adapted description: old CVS;
2008-12-01, by wenzelm
Methods intro_locales and unfold_locales apply to both old and new locales.
2008-12-01, by ballarin
code_include with attach
2008-12-01, by haftmann
experimental implementation of a well-sorting algorithm
2008-12-01, by haftmann
code_funcgr interface includes also sort algebra
2008-12-01, by haftmann
exported get_accesses (for diagnostic purpose)
2008-12-01, by haftmann
more means for algebra projection
2008-12-01, by haftmann
consider TeX spacing conventions for punctuation marks
2008-12-01, by haftmann
fix typed print translation for card UNIV
2008-11-30, by huffman
removed obsolete CVS instructions;
2008-11-30, by wenzelm
fixed spelling;
2008-11-30, by wenzelm
tuned;
2008-11-30, by wenzelm
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
2008-11-30, by wenzelm
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
2008-11-30, by wenzelm
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
2008-11-30, by wenzelm
misc tuning and clarification;
2008-11-30, by wenzelm
remove repository-only files;
2008-11-29, by wenzelm
more .hgignore entries;
2008-11-29, by wenzelm
tuned;
2008-11-29, by wenzelm
basic setup of .hgignore;
2008-11-29, by wenzelm
further notes;
2008-11-29, by wenzelm
Important notes on Mercurial repository access for Isabelle.
2008-11-29, by wenzelm
Floats for Real.
2008-11-29, by nipkow
new file float_syntax.ML
2008-11-29, by nipkow
New lexical item "float".
2008-11-29, by nipkow
Intro_locales_tac to simplify goals involving locale predicates.
2008-11-28, by ballarin
Ahere to modern naming conventions; proper treatment of internal vs external names.
2008-11-28, by ballarin
added Tim's find_theorems performance patch
2008-11-28, by kleing
FindTheorems performance improvements (from Timothy Bourke)
2008-11-28, by kleing
Perform higher-order pattern matching during round-up.
2008-11-28, by ballarin
Proper treatment of expressions with free arguments.
2008-11-27, by ballarin
Roundup bound.
2008-11-27, by ballarin
Tests for sublocale command.
2008-11-27, by ballarin
Sublocale command.
2008-11-27, by ballarin
Command to add dependencies, fixed processing of dependencies.
2008-11-27, by ballarin
Fixed strange indentation.
2008-11-27, by ballarin
add Algebraic and Universal to imports
2008-11-25, by huffman
separate run and cases combinators
2008-11-25, by huffman
renamed lemma compact_minimal to compact_bot_minimal;
2008-11-25, by huffman
renamed lemma compact_minimal to compact_bot_minimal
2008-11-25, by huffman
Use standard export function.
2008-11-25, by ballarin
Expression types cleaned up.
2008-11-25, by ballarin
Test for term patterns added.
2008-11-25, by ballarin
Expression types cleaned up, proper treatment of term patterns.
2008-11-25, by ballarin
check for more common errors first
2008-11-24, by krauss
improved error msg; tuned
2008-11-24, by krauss
removed "log" again, as IntInf.log2 already exists.
2008-11-24, by krauss
Some regression tests for theorem statements.
2008-11-24, by ballarin
Enable switching to new locales during session.
2008-11-24, by ballarin
Read/cert_statement for theorem statements.
2008-11-24, by ballarin
Generalised activation code.
2008-11-24, by ballarin
More ramifications of removal of 'includes' element.
2008-11-24, by ballarin
tuned;
2008-11-23, by wenzelm
eliminated finish_proof, keep pre/post normalization of results separate;
2008-11-23, by wenzelm
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
2008-11-23, by wenzelm
Regression tests for new locale implementation.
2008-11-21, by ballarin
add_locale functional.
2008-11-21, by ballarin
Added a line that was missing from the definition
2008-11-21, by paulson
added binary logarithm
2008-11-21, by krauss
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
2008-11-21, by paulson
Name.binding
2008-11-21, by haftmann
added optimizer
2008-11-20, by nipkow
reactivated some dead theories (based on hints by Mark Hillebrand);
2008-11-20, by wenzelm
Locale.local_note_qualified
2008-11-20, by haftmann
fact table now using name bindings
2008-11-20, by haftmann
dropped legacy naming code
2008-11-20, by haftmann
tuned name bindings
2008-11-20, by haftmann
using name bindings
2008-11-20, by haftmann
name spaces and name bindings
2008-11-20, by haftmann
Deleted debug message (PolyML).
2008-11-20, by ballarin
removed traces of former 'includes' element;
2008-11-20, by wenzelm
updated generated files;
2008-11-20, by wenzelm
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-11-20, by wenzelm
*** empty log message ***
2008-11-19, by nipkow
fixed
2008-11-19, by nipkow
Added new fold operator and renamed the old oe to fold_image.
2008-11-19, by nipkow
Type inference for elements through syntax module.
2008-11-19, by ballarin
Use 'if' in connection with 'is_some' and 'the'.
2008-11-19, by ballarin
Basic types not qualified.
2008-11-19, by ballarin
Enable switching to new locales during session.
2008-11-19, by ballarin
explicit inhabitance proof
2008-11-19, by haftmann
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
fulfill_proof/thm_proof: commuted lazyness;
2008-11-18, by wenzelm
removed lemmas called lemma1 and lemma2
2008-11-18, by krauss
force_proofs after cumulative use_thys;
2008-11-18, by wenzelm
signed_string_of_int for priorities;
2008-11-18, by wenzelm
added force_proofs;
2008-11-18, by wenzelm
added force_proofs (based on thms ever passed through enter_thms);
2008-11-18, by wenzelm
tuned;
2008-11-18, by wenzelm
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-11-18, by wenzelm
moved table of standard Isabelle symbols to isar-ref manual;
2008-11-18, by wenzelm
added isabelle-implementation manual;
2008-11-18, by wenzelm
disabled threads -- as advertized;
2008-11-18, by wenzelm
changes by Fabian Immler:
2008-11-18, by wenzelm
Code for switching to new locales.
2008-11-18, by ballarin
add_thmss
2008-11-18, by ballarin
Activate elements moved to element.ML.
2008-11-18, by ballarin
finish: force proofs;
2008-11-18, by wenzelm
finish_proof: undefined promises may occur here;
2008-11-17, by wenzelm
tuned promise/fullfill;
2008-11-17, by wenzelm
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
simplified thm_deps -- no need to build a graph datastructure;
2008-11-17, by wenzelm
removed Induct/Mutil.thy -- the file has been moved to AFP;
2008-11-17, by wenzelm
-> AFP
2008-11-17, by nipkow
tuned unfold_locales invocation
2008-11-17, by haftmann
explicit name morphism function for locale interpretation
2008-11-17, by haftmann
Name.name_with_prefix (temporarily)
2008-11-17, by haftmann
adjusted locale signature to *_cmd convention
2008-11-17, by haftmann
whitespace tuning
2008-11-17, by haftmann
Generic activation of locales.
2008-11-17, by ballarin
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
put_name/thm_proof: promises are filled with fulfilled proofs;
2008-11-16, by wenzelm
proof_body/pthm: removed redundant types field;
2008-11-16, by wenzelm
clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-16, by wenzelm
- Corrected order of quantification over Frees.
2008-11-16, by berghofe
Frees in PThms are now quantified in the order of their appearance in the
2008-11-16, by berghofe
adapted PThm and MinProof;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
retrieve thm deps from proof_body;
2008-11-15, by wenzelm
adapted PThm;
2008-11-15, by wenzelm
proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
refined notion of derivation, consiting of promises and proof_body;
2008-11-15, by wenzelm
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
2008-11-15, by wenzelm
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-11-15, by wenzelm
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
2008-11-15, by wenzelm
name_of_thm: Proofterm.fold_proof_atoms;
2008-11-15, by wenzelm
Thm.proof_of returns proof_body;
2008-11-15, by wenzelm
clean: added HOL-Main;
2008-11-15, by wenzelm
rewrite_proof: simplified simprocs (no name required);
2008-11-15, by wenzelm
multithreading support for polyml-5.2 actually disabled -- as advertized;
2008-11-15, by wenzelm
Initial part of locale reimplementation.
2008-11-14, by ballarin
Made local_note_prefix public.
2008-11-14, by ballarin
re-educated guess
2008-11-14, by haftmann
namify and name_decl combinators
2008-11-14, by haftmann
Name.is_nothing
2008-11-14, by haftmann
lemmas about dom and minus / insert
2008-11-14, by haftmann
added length_unique operation for code generation
2008-11-14, by haftmann
updated generated files;
2008-11-13, by wenzelm
removed "includes" element (lost update?);
2008-11-13, by wenzelm
updated generated files;
2008-11-13, by wenzelm
added section "Explicit instantiation within a subgoal context";
2008-11-13, by wenzelm
renamed "Rules" to "Object-level rules";
2008-11-13, by wenzelm
more on basic tactics;
2008-11-13, by wenzelm
basic ML reference for tactics;
2008-11-13, by wenzelm
added section "Tactics";
2008-11-13, by wenzelm
more contributors;
2008-11-13, by wenzelm
separate section "Inspecting the syntax" for print_syntax;
2008-11-13, by wenzelm
misc tuning of inner syntax;
2008-11-13, by wenzelm
added inner lexical syntax, reusing outer one;
2008-11-13, by wenzelm
misc tuning;
2008-11-13, by wenzelm
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
2008-11-13, by wenzelm
more tuning of Pure grammer;
2008-11-13, by wenzelm
updated and elaborated Pure grammer;
2008-11-13, by wenzelm
added Pure grammer (from old ref manual);
2008-11-13, by wenzelm
mixfix annotations: verbatim for special symbols;
2008-11-13, by wenzelm
added section "The Pure grammar" (incomplete version, based on old ref manual);
2008-11-13, by wenzelm
added section "Priority grammars" (variant from old ref manual);
2008-11-13, by wenzelm
added section "Co-regularity of type classes and arities" (variant from old ref manual);
2008-11-13, by wenzelm
minor tuning (according to old ref manual);
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
misc tuning and rearrangement of section "Printing logical entities";
2008-11-13, by wenzelm
fixed/tuned syntax for attribute "tagged";
2008-11-13, by wenzelm
added pretty printing options (from old ref manual);
2008-11-13, by wenzelm
separate chapter "Inner syntax --- the term language";
2008-11-13, by wenzelm
updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13, by wenzelm
unified use of declaration environment with IsarImplementation;
2008-11-13, by wenzelm
ignore ThyOutput.source flag;
2008-11-13, by wenzelm
added bind_thm, bind_thms;
2008-11-13, by wenzelm
tuned section "Incorporating ML code";
2008-11-13, by wenzelm
tuned section "Oracles";
2008-11-13, by wenzelm
tuned section arrangement;
2008-11-13, by wenzelm
moved section "Proof method expressions" to proof chapter;
2008-11-13, by wenzelm
more on mixfix annotations (updated material from old ref manual);
2008-11-13, by wenzelm
tuned;
2008-11-13, by wenzelm
moved section "Document preparation" to front;
2008-11-13, by wenzelm
updated section "Markup via command tags";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
renamed "formal comments" to "document comments";
2008-11-13, by wenzelm
tuned "Markup commands";
2008-11-13, by wenzelm
tuned intro of "Document preparation";
2008-11-13, by wenzelm
reworked "Defining Theories";
2008-11-13, by wenzelm
removed Assert.thy
2008-11-13, by haftmann
dropped superfluos eval_conv
2008-11-13, by haftmann
moved assert to Heap_Monad.thy
2008-11-13, by haftmann
simproc for let
2008-11-13, by haftmann
improved handling of !!/==> for eval and normalization
2008-11-13, by haftmann
proper name morphisms for locales
2008-11-13, by haftmann
consider prefixes for name bindings of simprocs (a first approximation)
2008-11-13, by haftmann
diagnostic output for name bindings
2008-11-13, by haftmann
Some modifications in code for proving arities to make it work for datatype
2008-11-13, by berghofe
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-11-12, by krauss
restruced naming code in anticipation of introduction of name morphisms
2008-11-10, by haftmann
more verbose element printing
2008-11-10, by haftmann
clarified comment
2008-11-10, by haftmann
Added support for parametric datatypes.
2008-11-10, by berghofe
Streamlined functions for accessing information about atoms.
2008-11-10, by berghofe
Some more functions for accessing information about atoms.
2008-11-10, by berghofe
Made doc compatible with the system.
2008-11-10, by ballarin
clarified verbatim vs. typewriter
2008-11-10, by haftmann
using explicit interpretaton prefix in Name.binding (still on the surface)
2008-11-10, by haftmann
explicit interpretation prefix in Name.binding
2008-11-10, by haftmann
tuned
2008-11-10, by haftmann
exported codegen_preproc
2008-11-07, by haftmann
Minor cleanup.
2008-11-06, by ballarin
Keyword 'includes' gone.
2008-11-06, by ballarin
tuned
2008-11-06, by nipkow
added lemma
2008-11-06, by nipkow
Added second tiling example.
2008-11-06, by nipkow
cleaned
2008-11-06, by haftmann
tuned
2008-11-06, by haftmann
class morphism stemming from locale interpretation
2008-11-06, by haftmann
improved verbatim mechanism
2008-11-03, by haftmann
Theorem "_" is now stored with open derivation.
2008-10-31, by berghofe
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
2008-10-31, by berghofe
Replaced arbitrary by undefined.
2008-10-31, by berghofe
Dropped context element 'includes'.
2008-10-30, by ballarin
adapted to strict pattern discipline
2008-10-29, by haftmann
explicit check for pattern discipline before code translation
2008-10-29, by haftmann
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28, by ballarin
restored incremental code generation
2008-10-28, by haftmann
slightly tuned
2008-10-28, by haftmann
assert that no class parameter is used as constructor
2008-10-28, by haftmann
cleanup code default attribute
2008-10-28, by haftmann
removed includes
2008-10-28, by haftmann
making SMLNJ happy
2008-10-28, by haftmann
The metis method no longer fails because the theorem is too trivial
2008-10-28, by paulson
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-28, by ballarin
metis proof
2008-10-27, by paulson
New-style locale expressions with instantiation (new file expression.ML).
2008-10-27, by ballarin
Hide path in constant name (workaround).
2008-10-27, by ballarin
explicit history for equations; tuned
2008-10-27, by haftmann
slightly tuned
2008-10-27, by haftmann
added rudimentary code generation
2008-10-27, by haftmann
sup_bot and inf_top
2008-10-27, by haftmann
Extension of interface: declarations_of.
2008-10-27, by ballarin
simplified user-defined class syntax
2008-10-24, by haftmann
more clever module names for code generation
2008-10-24, by haftmann
"fun" gained a more uniform status
2008-10-24, by haftmann
simplified syntax for class parameters
2008-10-24, by haftmann
tuned
2008-10-24, by haftmann
new classes "top" and "bot"
2008-10-24, by haftmann
tuned proof
2008-10-24, by haftmann
more clever module name aliasses for code generation
2008-10-24, by haftmann
"arbitrary" merely abbreviates undefined
2008-10-24, by haftmann
subst is a proper axiom again
2008-10-24, by haftmann
updated
2008-10-24, by haftmann
explicit namings for generated code
2008-10-24, by haftmann
Thm.get_def;
2008-10-23, by wenzelm
Thm.def_name;
2008-10-23, by wenzelm
multithreading support only for polyml-5.2.1 or later;
2008-10-23, by wenzelm
renamed get_axiom_i to axiom, removed obsolete get_axiom;
2008-10-23, by wenzelm
renamed Thm.get_axiom_i to Thm.axiom;
2008-10-23, by wenzelm
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23, by wenzelm
adapted Susp.peek;
2008-10-23, by wenzelm
thread-safe version, with non-critical evaluation;
2008-10-23, by wenzelm
do not open Susp;
2008-10-23, by wenzelm
switched parallel sessions to polyml-5.2.1;
2008-10-23, by wenzelm
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
2008-10-23, by wenzelm
updated to 5.2.1;
2008-10-22, by wenzelm
prove_instantiation_exit combinators
2008-10-22, by haftmann
added meet_sort_typ
2008-10-22, by haftmann
tuned
2008-10-22, by haftmann
code identifier namings are no longer imperative
2008-10-22, by haftmann
tuned typedef interface
2008-10-22, by haftmann
slightly tuned
2008-10-22, by haftmann
fixed
2008-10-22, by haftmann
less ambitious default for JEDIT_JAVA_OPTIONS;
2008-10-21, by wenzelm
JEDIT_OPTIONS: moved -settings to interface script (more robust);
2008-10-21, by wenzelm
make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
2008-10-21, by wenzelm
Added nominal_inductive2.
2008-10-21, by berghofe
Example for using the generalized version of nominal_inductive.
2008-10-21, by berghofe
Added theory W.
2008-10-21, by berghofe
More general, still experimental version of nominal_inductive for
2008-10-21, by berghofe
Added nominal_inductive2.ML
2008-10-21, by berghofe
added jEdit settings;
2008-10-21, by wenzelm
tuned usage line;
2008-10-21, by wenzelm
Isabelle/jEdit interface wrapper.
2008-10-21, by wenzelm
join results in isolation;
2008-10-21, by wenzelm
join_results: allow CRITICAL join of finished futures;
2008-10-21, by wenzelm
Future.join_result;
2008-10-21, by wenzelm
added Future.enabled check;
2008-10-21, by wenzelm
ThyOutput: export some auxiliary operations;
2008-10-21, by wenzelm
fixed proof
2008-10-20, by nipkow
added lemmas
2008-10-20, by nipkow
Names of variables in perm_eqs are now chosen more carefully to avoid
2008-10-19, by berghofe
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
2008-10-19, by berghofe
datatype_codegen now checks name of result type of constructor
2008-10-19, by berghofe
run a program in a modified environment;
2008-10-19, by wenzelm
reactivated HOL-Matrix;
2008-10-17, by wenzelm
tuned
2008-10-17, by haftmann
filled remaining gaps
2008-10-17, by haftmann
added type antiquotation
2008-10-17, by haftmann
tuned;
2008-10-16, by wenzelm
added dep for Concurrent/ROOT.ML;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
removed Locales;
2008-10-16, by wenzelm
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
2008-10-16, by wenzelm
added translations for SORT_CONSTRAINT
2008-10-16, by wenzelm
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added make;
2008-10-16, by wenzelm
maintain sort occurrences of declared terms;
2008-10-16, by wenzelm
added weaken_sorts;
2008-10-16, by wenzelm
added make, minimal_sorts;
2008-10-16, by wenzelm
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
2008-10-16, by wenzelm
added check_shyps, which reject pending sort hypotheses;
2008-10-16, by wenzelm
Drule.norm_hhf_eqs;
2008-10-16, by wenzelm
prove_common: include all sorts from context into statement, check shyps of result;
2008-10-16, by wenzelm
added rules for sort_constraint, include in norm_hhf_eqs;
2008-10-16, by wenzelm
tuned;
2008-10-16, by wenzelm
avoid accidental dependency of automated proof on sort equiv;
2008-10-16, by wenzelm
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
2008-10-16, by wenzelm
avoid CRITICAL with_path;
2008-10-16, by wenzelm
rewrite more proofs in Isar style
2008-10-16, by huffman
Removed ex/Locales.thy.
2008-10-16, by ballarin
More occurrences of 'includes' gone.
2008-10-16, by ballarin
Removed outdated locales tutorial.
2008-10-16, by ballarin
correct rounding
2008-10-16, by haftmann
circumvent some TeX problem
2008-10-16, by haftmann
only test HOL image for smlnj
2008-10-16, by kleing
tuned;
2008-10-15, by wenzelm
tuned;
2008-10-15, by wenzelm
generic ATP manager based on threads (by Fabian Immler);
2008-10-15, by wenzelm
added sledgehammer etc.;
2008-10-15, by wenzelm
removed obsolete Complex sessions;
2008-10-15, by wenzelm
figure for adaption
2008-10-15, by haftmann
Removed 'includes' (fixed).
2008-10-15, by ballarin
Removed 'includes'.
2008-10-15, by ballarin
give more time to do inital loggin and settings read
2008-10-15, by kleing
log start of test session
2008-10-15, by kleing
tuned interfaces -- plain prover function, without thread;
2008-10-14, by wenzelm
add_prover: plain prover function, without thread;
2008-10-14, by wenzelm
tuned AtpWrapper interfaces;
2008-10-14, by wenzelm
continued codegen tutorial
2008-10-14, by haftmann
renamed AtpThread to AtpWrapper;
2008-10-14, by wenzelm
adding preferences is now permissive;
2008-10-14, by wenzelm
tuned;
2008-10-14, by wenzelm
adding preferences is now permissive, no error handling here;
2008-10-14, by wenzelm
CRITICAL access to preferences;
2008-10-14, by wenzelm
export generic_pref etc.;
2008-10-14, by wenzelm
renamed kill_all to kill, in conformance with atp_kill command;
2008-10-14, by wenzelm
tuned comments;
2008-10-14, by wenzelm
added lemma
2008-10-14, by nipkow
Added liveness analysis
2008-10-14, by nipkow
info: back to plain printing;
2008-10-14, by wenzelm
added min_elem, upto;
2008-10-14, by wenzelm
added value;
2008-10-14, by wenzelm
simplified synchronized variable access;
2008-10-14, by wenzelm
State variables with synchronized access.
2008-10-13, by wenzelm
added generic combinator for synchronized evaluation (formerly in future.ML);
2008-10-13, by wenzelm
simplified implementation using Synchronized.var;
2008-10-13, by wenzelm
SimpleThread.synchronized;
2008-10-13, by wenzelm
added Concurrent/synchronized.ML;
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
** Update from Fabian **
2008-10-13, by wenzelm
tuned output;
2008-10-13, by wenzelm
tuned
2008-10-13, by haftmann
tuned
2008-10-13, by urbanc
change DISTPREFIX to not use yet another filesystem
2008-10-11, by kleing
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
tuned
2008-10-10, by haftmann
`code func` now just `code`
2008-10-10, by haftmann
some adaption
2008-10-10, by haftmann
using tikz pictures
2008-10-10, by haftmann
tuned default rules of (dvd)
2008-10-10, by haftmann
replaced str_of by general peek;
2008-10-09, by wenzelm
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-10-09, by wenzelm
fixed spelling;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
added enabled;
2008-10-09, by wenzelm
Multithreading.enabled;
2008-10-09, by wenzelm
moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-09, by wenzelm
added invalidate_group;
2008-10-09, by wenzelm
added fail-safe interrupt;
2008-10-09, by wenzelm
subject to Multithreading.enabled;
2008-10-09, by wenzelm
future result: Interrupt invalidates group, but pretends success otherwise;
2008-10-09, by wenzelm
added future_scheduler flag (tmp!), from skip_proofs.ML;
2008-10-09, by wenzelm
Dummy version of parallel list combinators -- plain sequential evaluation.
2008-10-09, by wenzelm
added Concurrent/par_list_dummy.ML;
2008-10-09, by wenzelm
improved performance of skolem cache, due to parallel map;
2008-10-09, by wenzelm
SimpleThread.interrupt;
2008-10-09, by wenzelm
report: back to single message;
2008-10-09, by wenzelm
added section label;
2008-10-09, by wenzelm
tuned
2008-10-09, by haftmann
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
2008-10-09, by kleing
removed legacy |>>>
2008-10-09, by haftmann
established canonical argument order in SML code generators
2008-10-09, by haftmann
established canonical argument order
2008-10-09, by haftmann
made SMLNJ happy
2008-10-09, by haftmann
less tracing;
2008-10-08, by wenzelm
Future.joint_results is already uninterruptible;
2008-10-08, by wenzelm
more careful handling of group interrupts;
2008-10-08, by wenzelm
use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;
2008-10-08, by wenzelm
added HOL-Main;
2008-10-08, by wenzelm
setmp_noncritical makes it work with future scheduler;
2008-10-08, by wenzelm
The result of the equality inference rule no longer undergoes factoring.
2008-10-08, by paulson
make the test for experimental sessions in isatest-check actually work
2008-10-08, by kleing
leave a log message when no snapshot is generated
2008-10-08, by kleing
clarified preprocessor policies
2008-10-07, by haftmann
arbitrary is undefined
2008-10-07, by haftmann
tuned whitespace
2008-10-07, by haftmann
only one theorem table for both code generators
2008-10-07, by haftmann
proper default codegen attribute
2008-10-07, by haftmann
tuned code setup
2008-10-07, by haftmann
code generator more liberal with respect to sort constraints of instance parameters
2008-10-07, by haftmann
more Isar for example
2008-10-07, by haftmann
tuned funpow code generation
2008-10-07, by haftmann
tuned min/max code generation
2008-10-07, by haftmann
dropped superfluous if
2008-10-07, by haftmann
tuned of_nat code generation
2008-10-07, by haftmann
re-introduces axiom subst
2008-10-07, by haftmann
corrected SML undefined
2008-10-07, by haftmann
updated to official version as of 07-Oct-2008;
2008-10-07, by wenzelm
fold_lines: more tuning, avoiding extra split_last;
2008-10-06, by wenzelm
extra check of PROOFGENERAL_HOME;
2008-10-06, by wenzelm
needs -b option for isabelle getenv
2008-10-05, by kleing
updated generated file;
2008-10-04, by wenzelm
tuned isabelle usage;
2008-10-04, by wenzelm
updated generated file;
2008-10-04, by wenzelm
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-04, by wenzelm
updated generated file;
2008-10-04, by wenzelm
replaced ISABELLE by ISABELLE_PROCESS;
2008-10-04, by wenzelm
ISABELLE_PROCESS commandline;
2008-10-04, by wenzelm
replaced ISATOOL by ISABELLE_TOOL;
2008-10-04, by wenzelm
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);
2008-10-04, by wenzelm
eliminated prompt messages;
2008-10-04, by wenzelm
added isabelle_tool version as basic integrity check of platform/distribution;
2008-10-04, by wenzelm
renamed isatool to isabelle_tool in programming interfaces;
2008-10-04, by wenzelm
Theory header keywords.
2008-10-04, by wenzelm
added Thy/thy_header.scala;
2008-10-04, by wenzelm
tuned quotes;
2008-10-03, by wenzelm
factor: proper padding of digits;
2008-10-03, by wenzelm
plain process_id function;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
removed obsolete Posix/Signal compatibility wrappers;
2008-10-03, by wenzelm
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
2008-10-03, by wenzelm
updated to new AtpManager;
2008-10-03, by wenzelm
operate on Proof.state, not Toplevel.state;
2008-10-03, by wenzelm
misc simplifcation and tuning;
2008-10-03, by wenzelm
perform atp_setups here;
2008-10-03, by wenzelm
updated generated file;
2008-10-03, by wenzelm
removed HOL-Plain -- already included in HOL;
2008-10-03, by wenzelm
removed spurious ResAtp.set_prover;
2008-10-03, by wenzelm
simplified thread creation via SimpleThread;
2008-10-03, by wenzelm
simplified thread creation via SimpleThread;
2008-10-03, by wenzelm
version of sledgehammer using threads instead of processes, misc cleanup;
2008-10-03, by wenzelm
removed old/unused setup of raw ATP oracles;
2008-10-03, by wenzelm
tuned;
2008-10-03, by wenzelm
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-10-03, by wenzelm
added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;
2008-10-03, by wenzelm
tuned tracing;
2008-10-03, by wenzelm
slower heartbeat;
2008-10-03, by wenzelm
added simple heartbeat thread;
2008-10-02, by wenzelm
time factor: one more digit;
2008-10-02, by wenzelm
more tuning of tracing messages;
2008-10-02, by wenzelm
include factor in timing report;
2008-10-02, by wenzelm
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
2008-10-02, by wenzelm
tracing: ignore failure of any kind;
2008-10-02, by wenzelm
tuned SYNCHRONIZED: outermost Exn.release;
2008-10-02, by wenzelm
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
2008-10-02, by wenzelm
added partiality section
2008-10-02, by haftmann
corrected class antiquotation
2008-10-02, by haftmann
max_threads_value always 1 for dummy version;
2008-10-02, by wenzelm
simplified Exn.EXCEPTIONS, flatten nested occurrences;
2008-10-02, by wenzelm
simplified Exn.EXCEPTIONS;
2008-10-02, by wenzelm
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
2008-10-02, by wenzelm
tuned
2008-10-02, by haftmann
Yet another proof of Newman's lemma, this time using the coherent logic prover.
2008-10-02, by berghofe
unit_source: more rigid parsing, stop after final qed;
2008-10-01, by wenzelm
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
2008-10-01, by wenzelm
replaced can_defer by is_relevant (negation);
2008-10-01, by wenzelm
datatype transition: internal trans field is maintained in reverse order;
2008-10-01, by wenzelm
future_proof: protect conclusion of deferred proof state;
2008-10-01, by wenzelm
future_schedule: back to one group for all loader tasks;
2008-10-01, by wenzelm
tuned comments;
2008-10-01, by wenzelm
fixed
2008-10-01, by haftmann
renamed promise to future, tuned related interfaces;
2008-10-01, by wenzelm
more robust treatment of Interrupt (cf. exn.ML);
2008-10-01, by wenzelm
more robust treatment of Interrupt;
2008-10-01, by wenzelm
more robust treatment of Interrupt (cf. exn.ML);
2008-10-01, by wenzelm
removed release_results (cf. Exn.release_all, Exn.release_first);
2008-10-01, by wenzelm
more precise join_futures, improved termination;
2008-10-01, by wenzelm
added more_antiquote.ML
2008-10-01, by haftmann
extract Isabelle dist name correctly
2008-10-01, by kleing
unit_source: explicit treatment of 'oops' proofs;
2008-09-30, by wenzelm
promise_proof: proper statement with empty vars;
2008-09-30, by wenzelm
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
2008-09-30, by wenzelm
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
2008-09-30, by wenzelm
added unit_source: commands with proof;
2008-09-30, by wenzelm
begin_proof: avoid race condition wrt. skip_proofs flag;
2008-09-30, by wenzelm
load_thy: Toplevel.excursion based on units of command/proof pairs;
2008-09-30, by wenzelm
more command categories;
2008-09-30, by wenzelm
renamed Future.fork_irrelevant to Future.fork_background;
2008-09-30, by wenzelm
export explicit joint_futures, removed Theory.at_end hook;
2008-09-30, by wenzelm
tuned
2008-09-30, by haftmann
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
2008-09-30, by wenzelm
Toplevel.commit_exit: position;
2008-09-30, by wenzelm
export setmp_thread_position;
2008-09-30, by wenzelm
simplified process_file, eliminated Toplevel.excursion;
2008-09-30, by wenzelm
clarified codegen interfaces
2008-09-30, by haftmann
tuned
2008-09-30, by haftmann
reorganized examples
2008-09-30, by haftmann
fixed slips
2008-09-30, by haftmann
re-canibalised manual
2008-09-30, by haftmann
slightly different command line for makedist_mercurial
2008-09-30, by kleing
put_thms: ContextPosition.set_visible false;
2008-09-29, by wenzelm
added type pp, which helps installing polymorphic pretty printers;
2008-09-29, by wenzelm
added str_of;
2008-09-29, by wenzelm
install_pp Future.T (polyml only);
2008-09-29, by wenzelm
report_token/parse_token: back to context-less version;
2008-09-29, by wenzelm
back to plain Position.report for regular references;
2008-09-29, by wenzelm
back to plain Position.report for regular references;
2008-09-29, by wenzelm
promise global proofs;
2008-09-29, by wenzelm
renamed report to report_visible;
2008-09-29, by wenzelm
code example: back to individual ML commands, which are now thread-safe;
2008-09-29, by wenzelm
ContextPosition.report;
2008-09-29, by wenzelm
target update: invisible context position avoids duplication of reports etc.;
2008-09-29, by wenzelm
Context position visibility.
2008-09-29, by wenzelm
added context_position.ML;
2008-09-29, by wenzelm
more precise redundancy check
2008-09-29, by haftmann
clarified dependencies between arith tools
2008-09-29, by haftmann
separate HOL-Main image
2008-09-29, by haftmann
polished code generator setup
2008-09-29, by haftmann
added theory antiquotation
2008-09-29, by haftmann
tuned comments;
2008-09-29, by wenzelm
handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-29, by wenzelm
added norm_export_morphism;
2008-09-29, by wenzelm
added exit_global, exit_result, exit_result_global;
2008-09-29, by wenzelm
LocalTheory.exit_global;
2008-09-29, by wenzelm
HOL no longer depends on HOL-Plain;
2008-09-28, by wenzelm
setmp_noncritical;
2008-09-28, by wenzelm
join earlier promises first;
2008-09-28, by wenzelm
proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28, by wenzelm
promise_result: enforce strictly sequential dependencies, via serial numbers;
2008-09-28, by wenzelm
do not cvs update for doc test (switching to mercurial, update done outside
2008-09-28, by kleing
use mercurial repository for isatest
2008-09-28, by kleing
thread_data: include thread name, export access;
2008-09-28, by wenzelm
setmp_noncritical;
2008-09-27, by wenzelm
dequeue_towards: return bound for unfinished tasks;
2008-09-27, by wenzelm
moved release_results to future.ML;
2008-09-27, by wenzelm
added release_results (formerly in par_list.ML);
2008-09-27, by wenzelm
Future.release_results;
2008-09-27, by wenzelm
more tracing;
2008-09-27, by wenzelm
Theory.checkpoint for main operations, admits concurrent proofs;
2008-09-27, by wenzelm
promise: include check into future body, i.e. joined results are always valid;
2008-09-27, by wenzelm
proper transfer of theorems that involve classes being instantiated here;
2008-09-27, by wenzelm
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
2008-09-27, by wenzelm
eliminated polymorphic equality;
2008-09-26, by wenzelm
added subset operation;
2008-09-26, by wenzelm
Added fresh_star_const.
2008-09-26, by berghofe
Added some more theorems to NominalData.
2008-09-26, by berghofe
Added some more lemmas that are useful in proof of strong induction rule.
2008-09-26, by berghofe
removed obsolete name convention "func"
2008-09-26, by haftmann
fixed typo
2008-09-26, by haftmann
clarified function transformator interface
2008-09-26, by haftmann
op = vs. eq
2008-09-26, by haftmann
moved future_scheduler flag to skip_proof.ML;
2008-09-25, by wenzelm
added future_scheduler (from thy_info.ML);
2008-09-25, by wenzelm
simplified promise;
2008-09-25, by wenzelm
simplified Thm.promise;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove;
2008-09-25, by wenzelm
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
2008-09-25, by wenzelm
circumvent problem with code redundancy
2008-09-25, by haftmann
clarifed redundancy policy
2008-09-25, by haftmann
tuned comments;
2008-09-25, by wenzelm
added release_results;
2008-09-25, by wenzelm
abtract types: plain datatype with opaque signature matching;
2008-09-25, by wenzelm
prove: error with original thread position;
2008-09-25, by wenzelm
explicit type OrdList.T;
2008-09-25, by wenzelm
(temporary workaround)
2008-09-25, by haftmann
(temporal deactivation)
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
non left-linear equations for nbe
2008-09-25, by haftmann
map_force
2008-09-25, by haftmann
matchess
2008-09-25, by haftmann
burrow_fst
2008-09-25, by haftmann
discontinued special treatment of op = vs. eq_class.eq
2008-09-25, by haftmann
report: produce individual status messages;
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
2008-09-24, by wenzelm
init: OuterKeyword.report;
2008-09-24, by wenzelm
prove_multi: immediate;
2008-09-23, by wenzelm
added promise_result, prove_promise;
2008-09-23, by wenzelm
Corrected call of SUBPROOF in coherent_tac that used wrong context.
2008-09-23, by berghofe
fixed outer syntax
2008-09-23, by haftmann
case default fallback for NBE
2008-09-23, by haftmann
fixed quickcheck parameter syntax
2008-09-23, by haftmann
renamed rtype to typerep
2008-09-23, by haftmann
added fold_rev;
2008-09-23, by wenzelm
added del_node, which is more efficient for sparse graphs;
2008-09-23, by wenzelm
IntGraph.del_node;
2008-09-23, by wenzelm
join_results: special case for empty list, works without multithreading;
2008-09-23, by wenzelm
added dest_deriv, removed external type deriv;
2008-09-23, by wenzelm
added conditional add_oracles, keep oracles_of_proof private;
2008-09-23, by wenzelm
Thm.proof_of;
2008-09-23, by wenzelm
Added coherent logic prover.
2008-09-22, by berghofe
New prover for coherent logic.
2008-09-22, by berghofe
Added setup for coherent logic prover.
2008-09-22, by berghofe
Added examples for coherent logic prover.
2008-09-22, by berghofe
Examples for coherent logic prover.
2008-09-22, by berghofe
made the perm_simp tactic to understand options such as (no_asm)
2008-09-22, by urbanc
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
added is_finished;
2008-09-22, by wenzelm
added Promise constructor, which is similar to Oracle but may be replaced later;
2008-09-22, by wenzelm
removed deriv.ML which is now incorporated into thm.ML;
2008-09-22, by wenzelm
added reject_draft;
2008-09-22, by wenzelm
type thm: fully internal derivation, no longer exported;
2008-09-22, by wenzelm
generic quickcheck framework
2008-09-22, by haftmann
TEMPORARY: make batch run happy
2008-09-22, by haftmann
absolute Library path
2008-09-22, by haftmann
different session branches for HOL-Plain vs. Plain
2008-09-22, by haftmann
temporary workaround for class constants
2008-09-22, by haftmann
corrected sort intersection
2008-09-22, by haftmann
some steps towards generic quickcheck framework
2008-09-22, by haftmann
fixed headers
2008-09-22, by haftmann
added some fragments from website
2008-09-22, by haftmann
made SML/NJ happy;
2008-09-20, by wenzelm
Isar toplevel editor model.
2008-09-19, by wenzelm
future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-19, by wenzelm
output_sync is now public;
2008-09-19, by wenzelm
added props_text (from isar_syn.ML);
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
moved Isar editor commands from isar_syn.ML to isar.ML;
2008-09-19, by wenzelm
added Isar/isar.scala;
2008-09-19, by wenzelm
avoid using implicit assumptions
2008-09-19, by huffman
add theory graph to ZF document
2008-09-19, by huffman
made SMLNJ happy
2008-09-19, by haftmann
jar: include sources;
2008-09-18, by wenzelm
tuned;
2008-09-18, by wenzelm
eval_term: CRITICAL due to eval_result;
2008-09-18, by wenzelm
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
2008-09-18, by wenzelm
updated generated file;
2008-09-18, by wenzelm
simplified oracle interface;
2008-09-18, by wenzelm
show: non-critical testing;
2008-09-18, by wenzelm
added deriv.ML: Abstract derivations based on raw proof terms.
2008-09-18, by wenzelm
termination prover for "fun" can be configured using context data.
2008-09-18, by krauss
updated generated file;
2008-09-18, by wenzelm
unchecked $ISABELLE_HOME_USER/etc/settings;
2008-09-18, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
threads work only for Poly/ML 5.2 or later;
2008-09-17, by wenzelm
* ML bindings produced via Isar commands are stored within the Isar context.
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
added inherit_env;
2008-09-17, by wenzelm
added map_contexts;
2008-09-17, by wenzelm
ML_prf: inherit env for all contexts within the proof;
2008-09-17, by wenzelm
shutdown only if Multithreading.available;
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
ML_Context.evaluate: proper context (for ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
2008-09-17, by wenzelm
simplified ML_Context.eval_in -- expect immutable Proof.context value;
2008-09-17, by wenzelm
explicit handling of ML environment within generic context;
2008-09-17, by wenzelm
added ML_prf;
2008-09-17, by wenzelm
use_text/use_file now depend on explicit ML name space;
2008-09-17, by wenzelm
ML name space -- dummy version of Poly/ML 5.2 facility.
2008-09-17, by wenzelm
added ML-Systems/ml_name_space.ML;
2008-09-17, by wenzelm
use ML_prf within proofs;
2008-09-17, by wenzelm
local @{context};
2008-09-17, by wenzelm
moved global ML bindings to global place;
2008-09-17, by wenzelm
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-17, by wenzelm
updated generated file;
2008-09-17, by wenzelm
wf_finite_psubset[simp], in_finite_psubset[simp]
2008-09-17, by krauss
Public interface to interpretation morphism.
2008-09-17, by ballarin
moved term_of syntax to separate theory
2008-09-17, by haftmann
removed obsolete theory
2008-09-17, by haftmann
added quickcheck.ML
2008-09-17, by haftmann
tuned comments;
2008-09-16, by wenzelm
multithreading for Poly/ML 5.1 is no longer supported;
2008-09-16, by wenzelm
tuned;
2008-09-16, by wenzelm
updated system manual;
2008-09-16, by wenzelm
Proof General / Emacs interface wrapper;
2008-09-16, by wenzelm
Proof General: option -I is obsolete;
2008-09-16, by wenzelm
added PROOFGENERAL_HOME;
2008-09-16, by wenzelm
separate emacs tool for Proof General / Emacs;
2008-09-16, by wenzelm
added quickcheck stub
2008-09-16, by haftmann
removed babel again
2008-09-16, by haftmann
celver code lemma avoid type ambiguity problem with Haskell
2008-09-16, by haftmann
a sophisticated char/nibble conversion combinator
2008-09-16, by haftmann
moved term_of syntax to separate theory
2008-09-16, by haftmann
SimpleThread.fork;
2008-09-16, by wenzelm
Simplified thread fork interface.
2008-09-16, by wenzelm
added Concurrent/simple_thread.ML;
2008-09-16, by wenzelm
updated generated file;
2008-09-16, by wenzelm
misc tuning and modernization;
2008-09-16, by wenzelm
check setting and tool;
2008-09-16, by wenzelm
Clearer separation of interpretation frontend and backend.
2008-09-16, by ballarin
No interpretation of locale with dangling type frees.
2008-09-16, by ballarin
Do not rely on locale assumption in interpretation.
2008-09-16, by ballarin
The metis method now fails in the usual manner, rather than raising an exception,
2008-09-16, by paulson
Fixed typo in locale declaration.
2008-09-16, by ballarin
added babel
2008-09-16, by haftmann
explicit size of characters
2008-09-16, by haftmann
dropped superfluous code lemmas
2008-09-16, by haftmann
evaluation using code generator
2008-09-16, by haftmann
generic value command
2008-09-16, by haftmann
converted symbols.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
converted misc.tex;
2008-09-15, by wenzelm
tuned;
2008-09-15, by wenzelm
generated files;
2008-09-15, by wenzelm
converted present.tex;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
load underscore package after iman etc.;
2008-09-15, by wenzelm
tuned comment;
2008-09-15, by wenzelm
added formal markup for setting, executable, tool;
2008-09-15, by wenzelm
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
2008-09-15, by wenzelm
converted basics.tex to theory file;
2008-09-15, by wenzelm
added isatt markup;
2008-09-15, by wenzelm
New outline for codegen tutorial -- draft
2008-09-14, by haftmann
added extern_fact (local or global);
2008-09-12, by wenzelm
print raw (internal) result names;
2008-09-12, by wenzelm
more procise printing of fact names;
2008-09-12, by wenzelm
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
2008-09-12, by wenzelm
cancel, shutdown: notify_all;
2008-09-11, by wenzelm
finish: Future.shutdown last;
2008-09-11, by wenzelm
eliminated requests, use global state variables uniformly;
2008-09-11, by wenzelm
finish: Future.shutdown;
2008-09-11, by wenzelm
added is_empty;
2008-09-11, by wenzelm
shutdown: global join-and-shutdown operation;
2008-09-11, by wenzelm
added focus, which indicates a particular collection of high-priority tasks;
2008-09-11, by wenzelm
some general notes on future values;
2008-09-11, by wenzelm
separate Concurrent/ROOT.ML;
2008-09-11, by wenzelm
Parallel list combinators.
2008-09-11, by wenzelm
added Concurrent/par_list.ML;
2008-09-11, by wenzelm
added interrupt_task (external id);
2008-09-10, by wenzelm
tuned;
2008-09-10, by wenzelm
future_schedule: uninterruptible join;
2008-09-10, by wenzelm
added future_scheduler (default false);
2008-09-10, by wenzelm
replaced join_all by join_results, which returns Exn.results;
2008-09-10, by wenzelm
workers: explicit activity flag;
2008-09-10, by wenzelm
future: allow explicit group;
2008-09-10, by wenzelm
cancel: invalidate group implicitly, via bool ref;
2008-09-10, by wenzelm
auto_flush: uniform block buffering for all output streams;
2008-09-10, by wenzelm
auto_flush stdout, stderr as well;
2008-09-09, by wenzelm
proper values of no_interrupts, regular_interrupts;
2008-09-09, by wenzelm
cancel: check_scheduler;
2008-09-09, by wenzelm
simplified dequeue: provide Thread.self internally;
2008-09-09, by wenzelm
eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09, by wenzelm
export get_first from underlying table;
2008-09-09, by wenzelm
out_stream: block-buffered, with separate autoflush thread (every 50ms);
2008-09-09, by wenzelm
babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
2008-09-09, by wenzelm
added comment
2008-09-09, by nipkow
human-readable printing of TaskQueue.task/group;
2008-09-09, by wenzelm
* Changed defaults for unify configuration options;
2008-09-09, by wenzelm
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
2008-09-09, by wenzelm
job: explicit 'ok' status -- false for canceled jobs;
2008-09-09, by wenzelm
Overall exception handler in order to insulate our users from low-level bugs.
2008-09-09, by paulson
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
2008-09-09, by paulson
Increasing the default limits in order to prevent unnecessary failures.
2008-09-09, by paulson
send: broadcast condition while locked!
2008-09-08, by wenzelm
proper signature constraint;
2008-09-08, by wenzelm
tuned Mailbox.send;
2008-09-08, by wenzelm
removed unused sync_interrupts;
2008-09-08, by wenzelm
moved thread data to future.ML (again);
2008-09-08, by wenzelm
more interrupt operations;
2008-09-08, by wenzelm
moved task, thread_data, group, queue to task_queue.ML;
2008-09-08, by wenzelm
Ordered queue of grouped tasks.
2008-09-08, by wenzelm
added Concurrent/task_queue.ML;
2008-09-08, by wenzelm
await: SYNCHRONIZED wait!
2008-09-08, by wenzelm
tuned check_cache;
2008-09-08, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
added sync_interrupts, regular_interrupts;
2008-09-07, by wenzelm
opaque signature constraint abstracts local type abbrev;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
added change_result;
2008-09-07, by wenzelm
Functional threads as future values.
2008-09-07, by wenzelm
added Concurrent/future.ML;
2008-09-07, by wenzelm
Default (mostly dummy) implementation of thread structures.
2008-09-07, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2008-09-07, by wenzelm
*** empty log message ***
2008-09-07, by wenzelm
explicit use of universal.ML and dummy_thread.ML;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
added no_interrupts;
2008-09-07, by wenzelm
tuned;
2008-09-07, by wenzelm
send: broadcast to all waiting threads;
2008-09-07, by wenzelm
added ML-Systems/thread_dummy.ML;
2008-09-07, by wenzelm
dropped "run" marker in monad syntax
2008-09-06, by haftmann
multithreading.ML provides dummy thread structures;
2008-09-05, by wenzelm
different bookkeeping for code equations
2008-09-05, by haftmann
renamed structure CodeTarget to Code_Target
2008-09-05, by haftmann
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
2008-09-05, by huffman
proper header;
2008-09-04, by wenzelm
added receive_timeout;
2008-09-04, by wenzelm
check WRAPPER_OUTPUT node type;
2008-09-04, by wenzelm
init: disallow "" as out stream;
2008-09-04, by wenzelm
fixed deps: no Concurrent/receiver.ML yet;
2008-09-04, by wenzelm
Concurrent message exchange via mailbox -- with unbounded queueing.
2008-09-04, by wenzelm
added Concurrent/mailbox.ML;
2008-09-04, by wenzelm
reorganize subsections
2008-09-04, by huffman
rename INF_drop_prefix to INFM_drop_prefix
2008-09-04, by huffman
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
2008-09-04, by huffman
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
2008-09-04, by huffman
tuned signature;
2008-09-04, by wenzelm
added General/queue.ML;
2008-09-04, by wenzelm
Efficient queues.
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML
2008-09-04, by wenzelm
multithreading.ML provides dummy thread structures;
2008-09-04, by wenzelm
moved Multithreading.task/schedule to Concurrent/schedule.ML;
2008-09-04, by wenzelm
provide dummy thread structures, including proper Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Thread.getLocal/setLocal;
2008-09-04, by wenzelm
Scheduling -- multiple threads working on a queue of tasks.
2008-09-04, by wenzelm
added Concurrent/schedule.ML;
2008-09-04, by wenzelm
update tags
2008-09-03, by convert-repo
use /home/isabelle/mercurial/bin/hg wrapper;
2008-09-03, by wenzelm
exclude large .mov files;
2008-09-03, by wenzelm
simplified add_axiom: no hyps;
2008-09-03, by wenzelm
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
2008-09-03, by wenzelm
axiomatization is now global-only;
2008-09-03, by wenzelm
added const_decl;
2008-09-03, by wenzelm
simplified specify_const: canonical args, global deps;
2008-09-03, by wenzelm
declare_const: Name.binding, store/report position;
2008-09-03, by wenzelm
Sign.declare_const: Name.binding;
2008-09-03, by wenzelm
removed ex/Puzzle
2008-09-03, by nipkow
added qualified: string -> binding -> binding;
2008-09-03, by wenzelm
Name.qualified;
2008-09-03, by wenzelm
theorem dependency hook: check previous state;
2008-09-03, by wenzelm
added pos_of;
2008-09-03, by wenzelm
-> AFP
2008-09-03, by nipkow
simplified Toplevel.add_hook: cover successful transactions only;
2008-09-03, by wenzelm
retired Ben Porter's DenumRat in favour of the shorter proof in
2008-09-03, by kleing
made SML/NJ happy;
2008-09-02, by wenzelm
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
2008-09-02, by wenzelm
* Generic Toplevel.add_hook interface allows to analyze the result of
2008-09-02, by wenzelm
Replaced Library/NatPair by Nat_Int_Bij.
2008-09-02, by nipkow
added new_thms_deps (operates on global facts, some name_hint approximation);
2008-09-02, by wenzelm
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
2008-09-02, by wenzelm
added add_hook interface for post-transition hooks;
2008-09-02, by wenzelm
tuned;
2008-09-02, by wenzelm
ProofDisplay.print_results;
2008-09-02, by wenzelm
no pervasive bindings;
2008-09-02, by wenzelm
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
2008-09-02, by nipkow
distributed literal code generation out of central infrastructure
2008-09-02, by haftmann
* Result facts now refer to the *full* internal name;
2008-09-02, by wenzelm
* Name bindings in higher specification mechanisms;
2008-09-02, by wenzelm
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-09-02, by wenzelm
updated generated file;
2008-09-02, by wenzelm
Interpretation commands no longer accept interpretation attributes.
2008-09-02, by ballarin
type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
explicit type Name.binding for higher-specification elements;
2008-09-02, by wenzelm
added binding;
2008-09-02, by wenzelm
added fixed_decl, fact_decl, local_fact_decl;
2008-09-02, by wenzelm
name_thm etc.: pass position;
2008-09-02, by wenzelm
added type binding -- generic name bindings;
2008-09-02, by wenzelm
name/var morphism operates on Name.binding;
2008-09-02, by wenzelm
adapted to class instantiation compliance
2008-09-02, by haftmann
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
2008-09-01, by nipkow
renamed lemma
2008-09-01, by nipkow
moved more lemmas here from AFP/Integration/Rats
2008-09-01, by nipkow
moved lemma into SetInterval where it belongs
2008-09-01, by nipkow
cleaned up code generation for {.._} and {..<_}
2008-09-01, by nipkow
*** empty log message ***
2008-09-01, by nipkow
extended interface to preferences to allow adding new ones
2008-09-01, by nipkow
Prover is set via menu now
2008-09-01, by nipkow
restructured code generation of literals
2008-09-01, by haftmann
IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
2008-08-29, by wenzelm
init: more explicit protocol of open/remove rendezvous;
2008-08-29, by wenzelm
use hardwired /tmp -- fifo only work on local file-system;
2008-08-29, by wenzelm
separate module for code output
2008-08-29, by haftmann
fixed names of class assumptions
2008-08-29, by haftmann
dropped parameter prefix for class theorems
2008-08-29, by haftmann
added charset (from isabelle_process.scala);
2008-08-28, by wenzelm
moved charset to isabelle_system.scala;
2008-08-28, by wenzelm
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
2008-08-28, by wenzelm
restructured and split code serializer module
2008-08-28, by haftmann
no parameter prefix for class interpretation
2008-08-28, by haftmann
updated
2008-08-28, by haftmann
tuned fold_lines;
2008-08-28, by wenzelm
fold_lines: simplified, more efficient due to String.fields;
2008-08-28, by wenzelm
rm fifo after open;
2008-08-28, by wenzelm
dummy setup for completion;
2008-08-28, by wenzelm
create named pipe;
2008-08-28, by wenzelm
added is_cygwin;
2008-08-28, by wenzelm
join stdout/stderr, eliminated Kind.STDERR;
2008-08-28, by wenzelm
explicit output stream, typically a named pipe;
2008-08-28, by wenzelm
refined option -W: output stream;
2008-08-28, by wenzelm
more function -> fun
2008-08-28, by krauss
quicksort: function -> fun
2008-08-28, by krauss
corrected some typos
2008-08-28, by krauss
fixed atom_to_xml: literal "name" attribute;
2008-08-28, by wenzelm
exported atom_to_xml;
2008-08-28, by wenzelm
changed Markup print mode to YXML -- explicitly decode messages before being issued;
2008-08-28, by wenzelm
tuned;
2008-08-28, by wenzelm
present_token: disable print_mode, which is YXML now;
2008-08-28, by wenzelm
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;
2008-08-28, by wenzelm
removed obsolete XML.Output workaround;
2008-08-28, by wenzelm
added get_int;
2008-08-28, by wenzelm
removed obsolete get_string;
2008-08-28, by wenzelm
removed obsolete ProofGeneral/pgml_isabelle.ML;
2008-08-28, by wenzelm
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
2008-08-27, by huffman
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
renamed Buffer.write to File.write_buffer;
2008-08-27, by wenzelm
load buffer.ML before file.ML;
2008-08-27, by wenzelm
replaced find_substring by first_field;
2008-08-27, by wenzelm
Consistent naming of theorems in interpretation.
2008-08-27, by ballarin
simplified parse_attrib (find_substring instead of space_explode);
2008-08-27, by wenzelm
added find_substring;
2008-08-27, by wenzelm
added HOL/ex/Numeral.thy
2008-08-27, by haftmann
get rid of tabs;
2008-08-27, by wenzelm
Property lists.
2008-08-27, by wenzelm
added General/properties.ML;
2008-08-27, by wenzelm
type Properties.T;
2008-08-27, by wenzelm
proper error message
2008-08-27, by haftmann
proper handling of type variabl names
2008-08-27, by haftmann
completing arities after subclass instance
2008-08-27, by haftmann
untabification
2008-08-27, by haftmann
tuned code generator setup
2008-08-27, by haftmann
added equivariance lemmas for ex1 and the
2008-08-27, by urbanc
add lemmas about Rats similar to those about Reals
2008-08-27, by huffman
move real_vector class proofs into vector_space and group_hom locales
2008-08-26, by huffman
added distributivity of relation composition over union [simp]
2008-08-26, by krauss
tuned append;
2008-08-26, by wenzelm
command: symbols.encode;
2008-08-26, by wenzelm
Reorganisation of registration code.
2008-08-26, by ballarin
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
2008-08-26, by krauss
purge classes after compilation;
2008-08-26, by wenzelm
renamed Isabelle-repository to isabelle;
2008-08-26, by wenzelm
Defined rationals (Rats) globally in Rational.
2008-08-26, by nipkow
replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
2008-08-26, by wenzelm
moved new Symbol.Interpretation into plugin;
2008-08-25, by wenzelm
promoted to EBPlugin;
2008-08-25, by wenzelm
explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;
2008-08-25, by wenzelm
tuned;
2008-08-25, by wenzelm
isabelle process: pick options/args from properties;
2008-08-25, by wenzelm
removed unused ConsolePlugin dependency;
2008-08-25, by wenzelm
simplified exceptions: use plain error function / RuntimeException;
2008-08-25, by wenzelm
added try_result;
2008-08-25, by wenzelm
misc reorganization;
2008-08-24, by wenzelm
Kind: added is_control;
2008-08-24, by wenzelm
get: allow null;
2008-08-24, by wenzelm
misc tuning of names;
2008-08-24, by wenzelm
rearranged source files;
2008-08-24, by wenzelm
init_message: class markup in message body, not header;
2008-08-24, by wenzelm
repackaged as isabelle.jedit;
2008-08-24, by wenzelm
untabify: silently turn tab into space if column information is unavailable;
2008-08-24, by wenzelm
corrected cache handling for class operations
2008-08-24, by haftmann
default replaces arbitrary
2008-08-24, by haftmann
tuned import order
2008-08-24, by haftmann
activated \<A>, \<a>, \<AA>, \<aa>;
2008-08-24, by wenzelm
* Isabelle/lib/classes/Pure.jar;
2008-08-23, by wenzelm
jars: removed obsolete Java process wrapper (cf. new Pure.jar);
2008-08-23, by wenzelm
obsolete;
2008-08-23, by wenzelm
obsolete -- superceded by Pure.jar (Scala version);
2008-08-23, by wenzelm
updated to Pure.jar;
2008-08-23, by wenzelm
added exec;
2008-08-23, by wenzelm
moved class Result into static object, removed dynamic tree method;
2008-08-23, by wenzelm
symbolic message markup;
2008-08-23, by wenzelm
renamed Markup.MALFORMED to Markup.BAD;
2008-08-23, by wenzelm
added position, messages;
2008-08-23, by wenzelm
added messages and process information;
2008-08-23, by wenzelm
Position properties.
2008-08-23, by wenzelm
added General/position.scala;
2008-08-23, by wenzelm
adapted to new IsabelleProcess from Pure.jar;
2008-08-23, by wenzelm
include ../../classes/Pure.jar;
2008-08-23, by wenzelm
added const Rational
2008-08-23, by nipkow
YXML.parse_failsafe;
2008-08-23, by wenzelm
shell_prefix: physical /bin/env on Cygwin;
2008-08-23, by wenzelm
removed full_markup mode (default);
2008-08-23, by wenzelm
added parse_failsafe;
2008-08-23, by wenzelm
refer to symbolic Markup;
2008-08-23, by wenzelm
Common markup elements.
2008-08-23, by wenzelm
added General/markup.scala;
2008-08-23, by wenzelm
BadVariable: toString;
2008-08-23, by wenzelm
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
2008-08-23, by wenzelm
append_string: proper backslash in character escapes;
2008-08-23, by wenzelm
added getenv;
2008-08-23, by wenzelm
tuned;
2008-08-23, by wenzelm
Isabelle outer syntax.
2008-08-23, by wenzelm
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
2008-08-23, by wenzelm
Isabelle process management -- always reactive due to multi-threaded I/O.
2008-08-23, by wenzelm
renamed DOM to document, add xml version and optional stylesheets;
2008-08-23, by wenzelm
tuned comments;
2008-08-22, by wenzelm
parse_attrib: proper index of name end!
2008-08-21, by wenzelm
tuned parse performance: avoid splitting terminal Y chunk;
2008-08-21, by wenzelm
parse_attrib: more efficient due to indexOf('=');
2008-08-21, by wenzelm
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
2008-08-21, by wenzelm
tuned comment;
2008-08-21, by wenzelm
added iterator over content;
2008-08-21, by wenzelm
proper ISABELLE_ROOT_JVM on Cygwin;
2008-08-21, by wenzelm
pattern: proper "." not "[.]"!
2008-08-21, by wenzelm
recode: proper result for unmatched symbols;
2008-08-21, by wenzelm
more robust pattern: look at longer matches first, added catch-all case;
2008-08-21, by wenzelm
added get_setting;
2008-08-21, by wenzelm
read_symbols: proper IsabelleSystem.platform_path;
2008-08-21, by wenzelm
added ISABELLE_ROOT_JVM;
2008-08-21, by wenzelm
Theorem on polynomial division and lemmas.
2008-08-18, by ballarin
removed parse_element -- no longer fits to liberal parse!
2008-08-17, by wenzelm
Minimalistic XML tree values.
2008-08-17, by wenzelm
Efficient text representation of XML trees.
2008-08-17, by wenzelm
added General/xml.scala, General/yxml.scala;
2008-08-17, by wenzelm
decode escaped symbols as well;
2008-08-17, by wenzelm
tuned Recoder;
2008-08-16, by wenzelm
more private fields;
2008-08-16, by wenzelm
jar: invoke scaladoc;
2008-08-16, by wenzelm
tuned comments;
2008-08-16, by wenzelm
use scala.collection.jcl.HashMap, which seems to be more efficient;
2008-08-16, by wenzelm
jar target: removed jvmpath -- does not work on Linux!?
2008-08-16, by wenzelm
add scala-library.jar if available;
2008-08-16, by wenzelm
jar target: jvmpath;
2008-08-16, by wenzelm
Isabelle system support.
2008-08-16, by wenzelm
reading symbol interpretation tables;
2008-08-16, by wenzelm
added Tools/isabelle_system.scala;
2008-08-16, by wenzelm
removed unused usage;
2008-08-16, by wenzelm
more robust handling of directory layout variants;
2008-08-16, by wenzelm
refined scala/java wrappers via isatool;
2008-08-16, by wenzelm
tuned abbrevs;
2008-08-16, by wenzelm
added ISABELLE_SCALA, ISABELLE_JAVA;
2008-08-16, by wenzelm
added ISABELLE_HOME_JVM;
2008-08-15, by wenzelm
proper jvmpath for cygwin;
2008-08-15, by wenzelm
proper RC;
2008-08-15, by wenzelm
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
2008-08-15, by wenzelm
refined JVM path wrappers;
2008-08-15, by wenzelm
added JVM components (Scala or Java);
2008-08-15, by wenzelm
tuned;
2008-08-15, by wenzelm
jars: build Pure.jar;
2008-08-15, by wenzelm
scan: proper recovery for escaped \\< symbols;
2008-08-15, by wenzelm
basic setup for Scala material;
2008-08-15, by wenzelm
Basic support for Isabelle symbols.
2008-08-15, by wenzelm
added some abbrevs;
2008-08-15, by wenzelm
removed redundant "symbol" property;
2008-08-15, by wenzelm
Default interpretation of some Isabelle symbols.
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
added ML_antiq, doc_antiq;
2008-08-15, by wenzelm
added README;
2008-08-15, by wenzelm
generated truetype font;
2008-08-15, by wenzelm
The Jerusalem font from 2004 -- unicode version.
2008-08-15, by wenzelm
args: explicit groups for file_name, theory_name;
2008-08-15, by wenzelm
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
2008-08-15, by wenzelm
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
2008-08-15, by wenzelm
token_kind: add Space, Comment;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
output_markup: check Markup.is_none;
2008-08-15, by wenzelm
added is_none;
2008-08-15, by wenzelm
Args.name_source(_position) for proper position information;
2008-08-15, by wenzelm
[source=false] for quoted antiquotation avoids quote-escapes in output;
2008-08-14, by wenzelm
report antiquotations;
2008-08-14, by wenzelm
tuned;
2008-08-14, by wenzelm
report ML_source;
2008-08-14, by wenzelm
renamed P.ml_source to P.ML_source;
2008-08-14, by wenzelm
report doc_source;
2008-08-14, by wenzelm
added ML_source, doc_source;
2008-08-14, by wenzelm
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14, by wenzelm
added source_of';
2008-08-14, by wenzelm
P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-14, by wenzelm
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-14, by wenzelm
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
retrieve_thms: transfer fact position to result;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-14, by wenzelm
made SML/NJ happy;
2008-08-14, by wenzelm
removed obsolete present_html -- now part of regular theory presentation;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
ProofDisplay.add_hook;
2008-08-13, by wenzelm
simplified present_local_theory/proof;
2008-08-13, by wenzelm
ProofDisplay.theory_results;
2008-08-13, by wenzelm
removed obsolete present_results;
2008-08-13, by wenzelm
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
2008-08-13, by wenzelm
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-13, by wenzelm
simplified markup commands;
2008-08-13, by wenzelm
simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-13, by wenzelm
added untabify_content;
2008-08-13, by wenzelm
tuned;
2008-08-13, by wenzelm
removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-08-13, by wenzelm
tuned document;
2008-08-13, by wenzelm
removed obsolete theorems;
2008-08-13, by wenzelm
Changed proof of strong induction rule to avoid infinite loop
2008-08-13, by berghofe
token_kind_markup: complete coverage;
2008-08-12, by wenzelm
OuterSyntax.scan: pass position;
2008-08-12, by wenzelm
message: ignored if body empty;
2008-08-12, by wenzelm
load_thy: removed obsolete dir argument;
2008-08-12, by wenzelm
abstract type span, tuned interfaces;
2008-08-12, by wenzelm
adapted ThyEdit operations;
2008-08-12, by wenzelm
added ignored, malformed transitions;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
Isabelle.command: inline former OuterSyntax.prepare_command;
2008-08-12, by wenzelm
load thy_edit.ML before outer_syntax.ML;
2008-08-12, by wenzelm
renamed unknown_span to malformed_span;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
updated generated file;
2008-08-12, by wenzelm
rudimentary code setup for set operations
2008-08-11, by haftmann
<applet>: more XHTML 1.0 Transitional conformance;
2008-08-11, by wenzelm
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11, by wenzelm
<pre>: removed xml:space, is already default;
2008-08-11, by wenzelm
produce XHTML 1.0 Transitional;
2008-08-11, by wenzelm
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-11, by wenzelm
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-11, by wenzelm
changed code setup
2008-08-11, by haftmann
re-arranged class dense_linear_order
2008-08-11, by haftmann
rudimentary code setup for set operations
2008-08-11, by haftmann
moved class wellorder to theory Orderings
2008-08-11, by haftmann
added parse_token (from proof_context.ML);
2008-08-10, by wenzelm
read_tyname/const/const_proper: report position;
2008-08-10, by wenzelm
pass position to get_fact;
2008-08-10, by wenzelm
pass token source to typ/term etc.;
2008-08-10, by wenzelm
added name property operation;
2008-08-10, by wenzelm
renamed ML_Lex.val_of to content_of;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
load args.ML later (after outer_parse.ML);
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
read_asts: report literal tokens;
2008-08-09, by wenzelm
tuned error message;
2008-08-09, by wenzelm
pos_of_token: Position.T;
2008-08-09, by wenzelm
dest: sort strings;
2008-08-09, by wenzelm
added literal;
2008-08-09, by wenzelm
read_token: more robust handling of empty text;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
tuned SymbolPos interface;
2008-08-09, by wenzelm
YXML.parse: allow text without markup, potentially empty;
2008-08-09, by wenzelm
added content;
2008-08-09, by wenzelm
added distance_of (permissive version);
2008-08-09, by wenzelm
count offset as well;
2008-08-08, by wenzelm
added offset/end_offset;
2008-08-08, by wenzelm
tuned formatting;
2008-08-08, by wenzelm
clean up dead code
2008-08-08, by krauss
made SML/NJ happy;
2008-08-08, by wenzelm
FundefLib.try_proof : attempt a proof and see if it works
2008-08-08, by krauss
added lemmas
2008-08-08, by nipkow
inner_syntax markup is back;
2008-08-07, by wenzelm
disabled inner_syntax markup for now;
2008-08-07, by wenzelm
added read_token -- with optional YXML encoding of position;
2008-08-07, by wenzelm
parse_token: use Syntax.read_token, pass full position information;
2008-08-07, by wenzelm
tuned;
2008-08-07, by wenzelm
map_default: more explicit scope;
2008-08-07, by wenzelm
datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07, by wenzelm
simplified Antiquote signature;
2008-08-07, by wenzelm
more precise positions due to SymbolsPos.implode_delim;
2008-08-07, by wenzelm
simplified Antiq: regular SymbolPos.text with position;
2008-08-07, by wenzelm
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
2008-08-07, by wenzelm
only increment column if valid;
2008-08-07, by wenzelm
install_pp Position.T;
2008-08-07, by wenzelm
Position.start;
2008-08-07, by wenzelm
SymbolPos.explode;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
Antiquote.read/read_arguments;
2008-08-07, by wenzelm
updated type of nested sources;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
adapted Scan.extend_lexicon/merge_lexicons;
2008-08-07, by wenzelm
renamed scan_antiquotes to read;
2008-08-07, by wenzelm
export not_eof;
2008-08-07, by wenzelm
reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-07, by wenzelm
advance: single argument (again);
2008-08-07, by wenzelm
Symbols with explicit position information.
2008-08-07, by wenzelm
added General/symbol_pos.ML;
2008-08-07, by wenzelm
Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06, by ballarin
added lemma
2008-08-06, by nipkow
made SML/NJ happy;
2008-08-06, by wenzelm
Reverted last change, since it caused incompatibilities.
2008-08-06, by berghofe
fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06, by wenzelm
T.end_position_of;
2008-08-06, by wenzelm
adapted Antiq;
2008-08-06, by wenzelm
parse_sort/typ/term/prop: report markup;
2008-08-06, by wenzelm
sort/typ/term/prop: inner_syntax markup encodes original source position;
2008-08-06, by wenzelm
removed obsolete range_of (already included in position);
2008-08-06, by wenzelm
report markup;
2008-08-06, by wenzelm
Antiq: inner vs. outer position;
2008-08-06, by wenzelm
of_properties: observe Markup.position_properties';
2008-08-06, by wenzelm
added position_properties';
2008-08-06, by wenzelm
token: maintain of source, which retains original position information;
2008-08-05, by wenzelm
moved OuterLex.count here;
2008-08-05, by wenzelm
improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05, by wenzelm
advance: operate on symbol list (less overhead);
2008-08-05, by wenzelm
added token;
2008-08-05, by wenzelm
fix HOL/ex/LexOrds.thy; add to regression
2008-08-05, by krauss
added report;
2008-08-05, by wenzelm
removed axiom;
2008-08-05, by wenzelm
get_fact: report position;
2008-08-05, by wenzelm
Facts.lookup: return static/dynamic status;
2008-08-05, by wenzelm
position scanner: encode token range;
2008-08-04, by wenzelm
added encode_range;
2008-08-04, by wenzelm
added end_line, end_column properties;
2008-08-04, by wenzelm
meta_subst: xsymbols make it work with clean Pure;
2008-08-04, by wenzelm
abstract type Scan.stopper, position taken from last input token;
2008-08-04, by wenzelm
abstract type Scan.stopper;
2008-08-04, by wenzelm
abstract type stopper, may depend on final input;
2008-08-04, by wenzelm
removed obsolete apply_theorems(_i);
2008-08-04, by wenzelm
tuned signature;
2008-08-04, by wenzelm
removed obsolete note_thms_cmd;
2008-08-04, by wenzelm
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
2008-08-04, by wenzelm
tuned description;
2008-08-04, by wenzelm
replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
2008-08-04, by wenzelm
Quoted terms in consts_code declarations are now preprocessed as well.
2008-08-04, by berghofe
Exported eval_wrapper.
2008-08-04, by berghofe
- corrected bogus comment for function inst_conj_all
2008-08-04, by berghofe
removed dead code
2008-08-04, by krauss
simplified prepare_command;
2008-08-04, by wenzelm
Isar.command: explicitly set transaction position, as required for prepare_command errors;
2008-08-04, by wenzelm
Updated locale tests.
2008-08-04, by ballarin
Generalised polynomial lemmas from cring to ring.
2008-08-01, by ballarin
Removed import and lparams from locale record.
2008-08-01, by ballarin
made setsum executable on int.
2008-08-01, by nipkow
Tuned (for the sake of a meaningless log entry).
2008-07-31, by ballarin
New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-30, by ballarin
added hint about writing "x : set xs".
2008-07-30, by nipkow
simple lifters
2008-07-30, by haftmann
dropped imperative monad bind
2008-07-30, by haftmann
facts_of
2008-07-30, by haftmann
improved morphism
2008-07-30, by haftmann
SML_imp, OCaml_imp
2008-07-30, by haftmann
clarified
2008-07-30, by haftmann
tuned
2008-07-30, by haftmann
Zorn's Lemma for partial orders.
2008-07-29, by ballarin
Definitions and some lemmas for reflexive orderings.
2008-07-29, by ballarin
Lemmas added
2008-07-29, by ballarin
New theory on divisibility.
2008-07-29, by ballarin
Renamed theorems;
2008-07-29, by ballarin
New theorems on summation.
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp].
2008-07-29, by ballarin
New theory on divisibility;
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp];
2008-07-29, by ballarin
Haskell now living in the RealWorld
2008-07-29, by haftmann
corrected Pure dependency
2008-07-29, by haftmann
added removeAll
2008-07-29, by nipkow
tuned; explicit export of element accessors
2008-07-29, by haftmann
PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-29, by haftmann
some steps towards explicit class target for canonical interpretation
2008-07-29, by haftmann
declare
2008-07-29, by haftmann
*** empty log message ***
2008-07-28, by nipkow
simplified a proof
2008-07-27, by urbanc
tuned function name
2008-07-26, by haftmann
tuned bootstrap order
2008-07-26, by haftmann
subclass now also works for subclasses with empty specificaton
2008-07-25, by haftmann
dropped PureThy.note; added PureThy.add_thm
2008-07-25, by haftmann
added class preorder
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
added explicit root theory; some tuning
2008-07-25, by haftmann
tuned
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
added explicit purge_data
2008-07-21, by haftmann
added code generation
2008-07-21, by haftmann
fixed code generator setup
2008-07-21, by haftmann
(adjusted)
2008-07-21, by haftmann
Tuned and corrected ideal_tac for algebra.
2008-07-21, by chaieb
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
2008-07-21, by chaieb
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
2008-07-21, by chaieb
Tuned and simplified proofs
2008-07-21, by chaieb
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
2008-07-21, by chaieb
Relevant rules added to algebra's context
2008-07-21, by chaieb
renamed item to span, renamed contructors;
2008-07-20, by wenzelm
adapted ThyEdit.span;
2008-07-20, by wenzelm
maintain token range;
2008-07-20, by wenzelm
tty loop: do not report status;
2008-07-20, by wenzelm
added type range;
2008-07-20, by wenzelm
renamed command span markup;
2008-07-20, by wenzelm
SideKickParsedData: minimal content;
2008-07-20, by wenzelm
(adjusted)
2008-07-20, by haftmann
(adjusted)
2008-07-20, by haftmann
added verification framework for the HeapMonad and quicksort as example for this framework
2008-07-19, by bulwahn
build jedit plugin only if jedit is available;
2008-07-19, by wenzelm
misc tuning;
2008-07-18, by wenzelm
more class instantiations
2008-07-18, by haftmann
refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-18, by haftmann
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-18, by haftmann
fixed Scala path;
2008-07-18, by wenzelm
tuned build order;
2008-07-17, by wenzelm
proper purge_tmp;
2008-07-17, by wenzelm
tuned message;
2008-07-17, by wenzelm
tuned line breaks (NB: generated text is inserted here);
2008-07-17, by wenzelm
proper usage message;
2008-07-17, by wenzelm
make Isabelle source distribution (via Mercurial);
2008-07-17, by wenzelm
explicit Distribution.changelog;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
ThyInfo.remove_thy;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
use ../isabelle.sty and ../isabellesym.sty;
2008-07-17, by wenzelm
tuned whitespace;
2008-07-17, by wenzelm
removed old checklist;
2008-07-17, by wenzelm
obsolete;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
discontinued maketags;
2008-07-17, by wenzelm
assume GNU tar and find;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
use ../isabellesym.sty, which is always available;
2008-07-17, by wenzelm
Admin/build browser;
2008-07-17, by wenzelm
less verbosity;
2008-07-17, by wenzelm
Administrative build -- finish Isabelle source distribution.
2008-07-17, by wenzelm
simplified proofs
2008-07-17, by krauss
beautified proofs
2008-07-17, by nipkow
added lemmas
2008-07-17, by nipkow
Added Standardization theory to nominal examples.
2008-07-16, by berghofe
Added Standardization theory.
2008-07-16, by berghofe
editor model: run interactively for now;
2008-07-16, by wenzelm
updated generated file;
2008-07-16, by wenzelm
identify: more informative id in Toplevel.debug mode;
2008-07-16, by wenzelm
shortlogentry/filelogentry: show shortdate and full description;
2008-07-16, by wenzelm
Removed uses of context element includes.
2008-07-16, by ballarin
added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-16, by wenzelm
export type id with no_id and create_command;
2008-07-16, by wenzelm
tuned;
2008-07-15, by wenzelm
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-15, by wenzelm
load thy_edit.ML before isar.ML;
2008-07-15, by wenzelm
modernized specifications and proofs;
2008-07-15, by wenzelm
Removed uses of context element includes.
2008-07-15, by ballarin
tuned
2008-07-15, by haftmann
tuned code theorem bookkeeping
2008-07-15, by haftmann
tuned changelogentry;
2008-07-15, by wenzelm
refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15, by wenzelm
support for command status;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
tuned;
2008-07-15, by wenzelm
simplified commit_exit;
2008-07-15, by wenzelm
simplified commit_exit: operate on previous node of final state, include warning here;
2008-07-15, by wenzelm
removed obsolete commit_exit;
2008-07-15, by wenzelm
added command 'linear_undo';
2008-07-15, by wenzelm
removed command 'redo';
2008-07-15, by wenzelm
adapted ThyInfo.end_theory;
2008-07-15, by wenzelm
dropped map; fixed swap
2008-07-15, by haftmann
curried gcd
2008-07-15, by haftmann
cover macbroy as well;
2008-07-14, by wenzelm
tuned filelogentry;
2008-07-14, by wenzelm
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14, by wenzelm
tuned message;
2008-07-14, by wenzelm
updated generated file;
2008-07-14, by wenzelm
inform_file_processed: Isar.init_point last!
2008-07-14, by wenzelm
removed HOL-Complex, which has been discontinued after Isabelle2008;
2008-07-14, by wenzelm
added HOL-Nominal image;
2008-07-14, by wenzelm
removed obsolete Pure/General/history.ML;
2008-07-14, by wenzelm
inform_file_processed: try harder not to fail, ensure
2008-07-14, by wenzelm
commit_exit: proper error;
2008-07-14, by wenzelm
export EXCURSION_FAIL;
2008-07-14, by wenzelm
dropped junk
2008-07-14, by haftmann
moved bootstrap of simplifier
2008-07-14, by haftmann
tuned
2008-07-14, by haftmann
end_theory: no result;
2008-07-14, by wenzelm
removed obsolete Toplevel.RESTART;
2008-07-14, by wenzelm
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
adapted IsarCmd.init_theory;
2008-07-14, by wenzelm
renamed theory to init_theory, removed obsolete kill argument;
2008-07-14, by wenzelm
added commit_exit;
2008-07-14, by wenzelm
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-07-14, by krauss
renamed conversions to _conv, tuned
2008-07-14, by krauss
Simplified proofs
2008-07-14, by chaieb
Simple theorems about zgcd moved to GCD.thy
2008-07-14, by chaieb
Theorem names as in IntPrimes.thy, also several theorems moved from there
2008-07-14, by chaieb
Fixed proofs.
2008-07-14, by chaieb
ProofNode.current
2008-07-14, by wenzelm
command 'redo' no longer available;
2008-07-14, by wenzelm
replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-14, by wenzelm
removed obsolete 'redo' command;
2008-07-14, by wenzelm
removed obsolete history commands;
2008-07-14, by wenzelm
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
2008-07-14, by wenzelm
obsolete (cf. proof_node.ML);
2008-07-14, by wenzelm
removed Isar/proof_history.ML;
2008-07-14, by wenzelm
added further simple interfaces
2008-07-14, by haftmann
simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-14, by haftmann
unified curried gcd, lcm, zgcd, zlcm
2008-07-14, by haftmann
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
instance real_field < field_char_0;
2008-07-11, by huffman
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-11, by haftmann
Fract now total; improved code generator setup
2008-07-11, by haftmann
simple inheritance concept
2008-07-11, by haftmann
tuned thyname lookup
2008-07-11, by haftmann
fixed layout
2008-07-11, by haftmann
explicit completions of arities
2008-07-11, by haftmann
tuned order
2008-07-11, by haftmann
antiquotation
2008-07-11, by haftmann
improved code generator setup
2008-07-11, by haftmann
explicit dependency
2008-07-11, by haftmann
class instead of axclass
2008-07-11, by haftmann
tuned import
2008-07-11, by haftmann
separate class dvd for divisibility predicate
2008-07-11, by haftmann
temporarily disable at-sml-dev-p
2008-07-11, by kleing
updated generated file;
2008-07-10, by wenzelm
restart: Isar.init_point;
2008-07-10, by wenzelm
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
2008-07-10, by wenzelm
activated new versions of undo, kill_proof;
2008-07-10, by wenzelm
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
2008-07-10, by wenzelm
added print;
2008-07-10, by wenzelm
added ProofGeneral.isar_kill_proof;
2008-07-10, by wenzelm
added Isar.init_point, Isar.kill;
2008-07-10, by wenzelm
export init_point;
2008-07-10, by wenzelm
added Isar.linear_undo;
2008-07-10, by wenzelm
tuned;
2008-07-10, by wenzelm
tty interaction: do not move point after error;
2008-07-10, by wenzelm
change_lexicons: no verbosity;
2008-07-10, by wenzelm
added Isar.undo, which emulates old-style undo on global tty state;
2008-07-10, by wenzelm
provide old-style undo operation (still unused);
2008-07-10, by wenzelm
added prompt markup;
2008-07-10, by wenzelm
@{lemma}: allow terminal method;
2008-07-10, by wenzelm
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-07-10, by wenzelm
added is_diag;
2008-07-10, by wenzelm
slightly improved @{lemma} (both for latex and ML);
2008-07-10, by wenzelm
misc tuning;
2008-07-10, by wenzelm
Fixed (harmless) typo in closing *}.
2008-07-10, by ballarin
by intro_locales -> ..
2008-07-10, by huffman
instance real_field < field_char_0
2008-07-10, by huffman
remove redundant lemmas about cmod
2008-07-09, by huffman
removed owner;
2008-07-09, by wenzelm
tuned description;
2008-07-09, by wenzelm
changes wrt. gitweb style;
2008-07-09, by wenzelm
style = isabelle (based on gitweb);
2008-07-09, by wenzelm
rearrange instantiations
2008-07-09, by huffman
added get_first;
2008-07-09, by wenzelm
updated generated file;
2008-07-08, by wenzelm
updated generated file;
2008-07-08, by wenzelm
fix more typos
2008-07-08, by huffman
fix another typo
2008-07-08, by huffman
fix typo
2008-07-08, by huffman
updated generated file;
2008-07-08, by wenzelm
global commands: explicit graph;
2008-07-08, by wenzelm
export str_of;
2008-07-08, by wenzelm
clarified code
2008-07-08, by haftmann
exported weaken combinator
2008-07-08, by haftmann
refined arity property concept
2008-07-08, by haftmann
fix: using IntInf.int for SML
2008-07-08, by haftmann
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
removed obsolete touch_child_thys;
2008-07-08, by wenzelm
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
more qualified ThyInfo names;
2008-07-08, by wenzelm
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
2008-07-08, by wenzelm
removed unused href_opt_name;
2008-07-08, by wenzelm
migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware
2008-07-08, by kleing
retired mac-sml-dev.
2008-07-07, by kleing
absolute imports of HOL/*.thy theories
2008-07-07, by haftmann
prefer theorem names without numbers
2008-07-04, by huffman
HOL-NSA
2008-07-04, by huffman
added marginal setup for code generation
2008-07-04, by haftmann
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
2008-07-03, by huffman
less
more
|
(0)
-30000
-10000
-4096
+4096
+10000
+30000
tip