Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-2048
+2048
+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.
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
less
more
|
(0)
-30000
-10000
-2048
+2048
+10000
+30000
tip