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