Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-960
+960
+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 print_stmts;
2006-03-14, by wenzelm
added pretty_statement;
2006-03-14, by wenzelm
added command, keyword;
2006-03-14, by wenzelm
Output.add_mode: keyword component;
2006-03-14, by wenzelm
string_of_mixfix;
2006-03-14, by wenzelm
print_statement;
2006-03-14, by wenzelm
added remove_trrules(_i);
2006-03-14, by wenzelm
added is_elim (from Provers/classical.ML);
2006-03-14, by wenzelm
added 'no_translations';
2006-03-14, by wenzelm
added pretty_stmt;
2006-03-14, by wenzelm
declared_const: check for type constraint only, i.e. admit abbreviations as well;
2006-03-14, by wenzelm
ObjectLogic.is_elim;
2006-03-14, by wenzelm
tuned constdecl;
2006-03-14, by wenzelm
updated;
2006-03-14, by wenzelm
Pure: no_translations;
2006-03-14, by wenzelm
refined representation of instance dictionaries
2006-03-14, by haftmann
entry for Library/AssocList
2006-03-13, by schirmer
First version of function for defining graph of iteration combinator.
2006-03-13, by berghofe
got rid of type Sign.sg;
2006-03-11, by wenzelm
renamed plus to add;
2006-03-11, by wenzelm
renamed const minus to subtract;
2006-03-11, by wenzelm
simplified AxClass interfaces;
2006-03-11, by wenzelm
added axclass_instance_XXX (from axclass.ML);
2006-03-11, by wenzelm
*** empty log message ***
2006-03-11, by wenzelm
added read_class, read/cert_classrel/arity (from axclass.ML);
2006-03-11, by wenzelm
moved read_class, read/cert_classrel/arity to sign.ML;
2006-03-11, by wenzelm
use axclass.ML earlier (in Isar/ROOT.ML);
2006-03-11, by wenzelm
nbe: no_document;
2006-03-11, by wenzelm
tuned;
2006-03-10, by wenzelm
exporting reapAll and killChild
2006-03-10, by paulson
text delimiter fixed
2006-03-10, by webertj
comment delimiter fixed
2006-03-10, by webertj
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
2006-03-10, by webertj
fix for document preparation
2006-03-10, by haftmann
Added Library/AssocList.thy
2006-03-10, by schirmer
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-10, by haftmann
Changed some warnings to debug messages
2006-03-10, by paulson
Frequency analysis of constants (with types).
2006-03-10, by paulson
Shortened the exception messages from assume.
2006-03-10, by mengj
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
2006-03-10, by mengj
added many simple lemmas
2006-03-10, by huffman
Added more functions to the signature and tidied up some functions.
2006-03-09, by mengj
tuned;
2006-03-08, by wenzelm
tuned some proofs
2006-03-08, by urbanc
select_goals: split original conjunctions;
2006-03-08, by wenzelm
method: goal restriction defaults to [1];
2006-03-08, by wenzelm
infer_derivs: avoid allocating empty MinProof;
2006-03-08, by wenzelm
tuned;
2006-03-08, by wenzelm
Isar/method: goal restriction;
2006-03-08, by wenzelm
constdecl: always allow 'where';
2006-03-08, by wenzelm
deleted some proofs "on comment"
2006-03-08, by urbanc
tuned some proofs
2006-03-08, by urbanc
tuned some of the proofs about fresh_fun
2006-03-08, by urbanc
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
Frequency strategy. Revised indentation, etc.
2006-03-08, by paulson
*** empty log message ***
2006-03-08, by nipkow
added ROOT.ML
2006-03-07, by obua
Indentation
2006-03-07, by paulson
Tidying and restructuring.
2006-03-07, by paulson
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
2006-03-07, by paulson
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
2006-03-07, by paulson
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
2006-03-07, by paulson
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-03-07, by paulson
Added HOL-ZF to Isabelle.
2006-03-07, by obua
substantial improvement in codegen iml
2006-03-07, by haftmann
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
2006-03-07, by mengj
relevance_filter takes input axioms as Term.term.
2006-03-07, by mengj
Proof reconstruction now only takes names of theorems as input.
2006-03-07, by mengj
Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-03-07, by mengj
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-07, by mengj
Added functions to retrieve local and global atpset rules.
2006-03-07, by mengj
Moved the settings for ATP time limit to res_atp.ML
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
SELECT_GOAL: fixed trivial case;
2006-03-05, by wenzelm
fixed a typo in a comment
2006-03-05, by webertj
tuned;
2006-03-04, by wenzelm
method: SelectGoals;
2006-03-04, by wenzelm
method: syntax for SelectGoals;
2006-03-04, by wenzelm
text: added SelectGoals;
2006-03-04, by wenzelm
tuned conj_curry;
2006-03-04, by wenzelm
added extract, retrofit;
2006-03-04, by wenzelm
added mk_conjunction;
2006-03-04, by wenzelm
method: restriction to first n sub-goals;
2006-03-04, by wenzelm
minor changes
2006-03-03, by nipkow
more examples
2006-03-03, by nipkow
changed and retracted change of location of code lemmas.
2006-03-03, by nipkow
ignore repeated vars on lhs, cleanup
2006-03-03, by nipkow
improvements for nbe
2006-03-03, by haftmann
reformatting
2006-03-02, by paulson
subset_refl now included using the atp attribute
2006-03-02, by paulson
moved the "use" directive
2006-03-02, by paulson
fixed the bugs itroduced by the previous commit
2006-03-02, by urbanc
made some small changes to generate nicer latex-output
2006-03-02, by urbanc
split the files
2006-03-02, by urbanc
Added in a signature.
2006-03-02, by mengj
fixed a problem where a permutation is not analysed
2006-03-01, by urbanc
streamlined the proof
2006-03-01, by urbanc
refined representation of codegen intermediate language
2006-03-01, by haftmann
some small tunings
2006-03-01, by urbanc
added fresh_fun_eqvt theorem to the theorem collection
2006-03-01, by urbanc
added initialisation-code for finite_guess
2006-03-01, by urbanc
made some small tunings in the decision-procedure
2006-03-01, by urbanc
Added setup for "atpset" (a rule set for ATPs).
2006-03-01, by mengj
Added file Tools/res_atpset.ML.
2006-03-01, by mengj
Merged HOL and FOL clauses and combined some functions.
2006-03-01, by mengj
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
2006-03-01, by mengj
some minor tuning on the proofs
2006-03-01, by urbanc
initial commit (especially 2nd half needs to be cleaned up)
2006-02-28, by urbanc
removal of theory blacklist
2006-02-28, by paulson
new order for arity clauses
2006-02-28, by paulson
fixed but in freeze_spec
2006-02-28, by paulson
splitting up METAHYPS into smaller functions
2006-02-28, by paulson
typos
2006-02-28, by paulson
added a finite_guess tactic, which solves
2006-02-27, by urbanc
class package and codegen refinements
2006-02-27, by haftmann
added nbe
2006-02-27, by haftmann
added temp. nbe test
2006-02-27, by nipkow
added nbe, updated neb_*
2006-02-27, by nipkow
added nbe
2006-02-27, by nipkow
Typo.
2006-02-27, by ballarin
added support for arbitrary atoms in the simproc
2006-02-27, by urbanc
put_thms: do_index;
2006-02-26, by wenzelm
rewrite_goals_rule_aux: actually use prems if present;
2006-02-26, by wenzelm
add_local: do_index;
2006-02-26, by wenzelm
replaced the lemma at_two by at_different;
2006-02-26, by urbanc
improved the decision-procedure for permutations;
2006-02-26, by urbanc
improved codegen bootstrap
2006-02-25, by haftmann
change in codegen syntax
2006-02-25, by haftmann
some refinements
2006-02-25, by haftmann
added more detailed data to consts
2006-02-25, by haftmann
Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24, by berghofe
Adapted to Florian's recent changes to the AxClass package.
2006-02-24, by berghofe
added lemmas
2006-02-23, by urbanc
make SML/NJ happy;
2006-02-23, by wenzelm
Default type level is T_FULL now.
2006-02-23, by mengj
eprover removes tmp files too.
2006-02-23, by mengj
vampire/eprover methods can now be applied repeatedly until they fail.
2006-02-23, by mengj
removed obsolete meta_conjunction_tr';
2006-02-22, by wenzelm
rew: handle conjunctionI/D1/D2;
2006-02-22, by wenzelm
simplified Pure conjunction, based on actual const;
2006-02-22, by wenzelm
removed rename_indexes_wrt;
2006-02-22, by wenzelm
renamed class_axms to class_intros;
2006-02-22, by wenzelm
tuned proofs;
2006-02-22, by wenzelm
simplified Pure conjunction;
2006-02-22, by wenzelm
not_equal: replaced syntax translation by abbreviation;
2006-02-22, by wenzelm
abandoned merge_alists' in favour of generic AList.merge
2006-02-22, by haftmann
added Tools/nbe, fixes
2006-02-21, by nipkow
added Tools/nbe
2006-02-21, by nipkow
New normalization-by-evaluation package
2006-02-21, by nipkow
distinct (op =);
2006-02-21, by wenzelm
fixed
2006-02-20, by kleing
Inclusion of subset_refl in ATP calls
2006-02-20, by paulson
Fix variable-naming bug (?) by removing a needless recursive call
2006-02-20, by paulson
slight code generator serialization improvements
2006-02-20, by haftmann
moved intro_classes from AxClass to ClassPackage
2006-02-20, by haftmann
fixed document
2006-02-19, by kleing
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
2006-02-19, by kleing
added a few lemmas to do with permutation-equivalence for the
2006-02-19, by urbanc
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
2006-02-19, by kleing
use minimal imports
2006-02-19, by huffman
use qualified name for return
2006-02-19, by huffman
dest_def: tuned error msg;
2006-02-18, by wenzelm
const constraints: provide TFrees instead of TVars,
2006-02-17, by wenzelm
checkpoint/copy_node: reset body context;
2006-02-17, by wenzelm
global_qeds: transfer body context;
2006-02-17, by wenzelm
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
constrain: assert const declaration, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
removed Import/lazy_scan.ML;
2006-02-17, by wenzelm
hyperlinks in the PDF work now
2006-02-17, by paulson
replaced Symbol.explode by explode
2006-02-17, by obua
updated mailing list archive link
2006-02-17, by haftmann
use monomorphic sequences / scanners
2006-02-17, by obua
make maybe into a real type constructor; remove monad syntax
2006-02-17, by huffman
use VectorScannerSeq instead of ListScannerSeq in xml.ML
2006-02-16, by obua
removed lazy_scan
2006-02-16, by obua
improved scanning
2006-02-16, by obua
tuned;
2006-02-16, by wenzelm
Abstract Natural Numbers with polymorphic recursion.
2006-02-16, by wenzelm
new-style definitions/abbreviations;
2006-02-16, by wenzelm
added ex/Abstract_NAT.thy;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
removed silly stuff
2006-02-16, by haftmann
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
2006-02-16, by wenzelm
added abbreviation(_i);
2006-02-16, by wenzelm
added put_thms_internal: local_naming, no fact index;
2006-02-16, by wenzelm
added put_thms_internal;
2006-02-16, by wenzelm
added abbrev element;
2006-02-16, by wenzelm
added 'abbreviation';
2006-02-16, by wenzelm
added premsN;
2006-02-16, by wenzelm
Proof.put_thms_internal;
2006-02-16, by wenzelm
removed pointless replace;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
dest_def: actually return beta-eta contracted equation;
2006-02-16, by wenzelm
derived specifications: definition, abbreviation, axiomatization;
2006-02-16, by wenzelm
updated;
2006-02-16, by wenzelm
cache improvements
2006-02-16, by obua
variable counter is now also cached
2006-02-16, by obua
adapted to kernel changes
2006-02-16, by obua
tuned subst_bound(s);
2006-02-16, by wenzelm
fixed bugs, added caching
2006-02-15, by obua
added cases_node;
2006-02-15, by wenzelm
replaced qualified_force_prefix to sticky_prefix;
2006-02-15, by wenzelm
removed distinct, renamed gen_distinct to distinct;
2006-02-15, by wenzelm
check_text: Toplevel.node option;
2006-02-15, by wenzelm
init/exit no longer change the theory (no naming);
2006-02-15, by wenzelm
evaluate antiquotes depending on Toplevel.node option;
2006-02-15, by wenzelm
simplified presentation commands;
2006-02-15, by wenzelm
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
2006-02-15, by wenzelm
removed qualified_force_prefix;
2006-02-15, by wenzelm
replaced qualified_force_prefix to sticky_prefix;
2006-02-15, by wenzelm
chop is no longer pervasive;
2006-02-15, by wenzelm
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
2006-02-15, by wenzelm
added distinct_prems_rl;
2006-02-15, by wenzelm
specifications_of: avoid partiality;
2006-02-15, by wenzelm
counter example: avoid vacuous trace;
2006-02-15, by wenzelm
cannot use section before setup;
2006-02-15, by wenzelm
used Tactic.distinct_subgoals_tac;
2006-02-15, by wenzelm
removed distinct, renamed gen_distinct to distinct;
2006-02-15, by wenzelm
added lemma pt_perm_compose'
2006-02-15, by urbanc
got rid of superfluous linorder_neqE-instance for int.
2006-02-15, by nipkow
typo in a comment fixed
2006-02-15, by webertj
exported some interfaces useful for other code generator approaches
2006-02-15, by haftmann
some fixes
2006-02-15, by haftmann
exported specifications_of
2006-02-15, by haftmann
added theory of executable rational numbers
2006-02-14, by haftmann
improved handling of iml abstractions
2006-02-14, by haftmann
fixed tracing
2006-02-14, by paulson
Adapted to Context.generic syntax.
2006-02-13, by berghofe
Fixed a bug of type unification.
2006-02-13, by mengj
* ML/Pure/General: improved join interface for tables;
2006-02-12, by wenzelm
consts: maintain thy version for efficient transfer;
2006-02-12, by wenzelm
tuned;
2006-02-12, by wenzelm
export exception SAME (for join);
2006-02-12, by wenzelm
low-level tuning of merge: maintain identity of accesses;
2006-02-12, by wenzelm
share exception UNDEF with Table;
2006-02-12, by wenzelm
structure Datatab: private copy avoids potential conflict of table exceptions;
2006-02-12, by wenzelm
added eq_consts;
2006-02-12, by wenzelm
minor tuning of proofs, notably induct;
2006-02-12, by wenzelm
simplified TableFun.join;
2006-02-12, by wenzelm
\usepackage{amssymb};
2006-02-12, by wenzelm
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
2006-02-12, by kleing
* moved ThreeDivides from Isar_examples to better suited HOL/ex
2006-02-12, by kleing
divisibility by 3 theorem, contributed by Benjamin Porter,
2006-02-12, by kleing
replaced mixfix_conflict by mixfix_content;
2006-02-11, by wenzelm
added map_theory;
2006-02-11, by wenzelm
added abbreviations: activated by init, no expressions yet;
2006-02-11, by wenzelm
added restore;
2006-02-11, by wenzelm
tuned mixfixes, mixfix_conflict;
2006-02-11, by wenzelm
removed custom_accesses;
2006-02-11, by wenzelm
added variant_name;
2006-02-11, by wenzelm
removed custom_accesses;
2006-02-11, by wenzelm
tuned;
2006-02-11, by wenzelm
added chop (sane version of splitAt);
2006-02-11, by wenzelm
Changed some code due to changes in reduce_axiomsN.ML.
2006-02-11, by mengj
Added another filter strategy.
2006-02-11, by mengj
improved code generator devarification
2006-02-10, by haftmann
statement: improved error msg;
2006-02-10, by wenzelm
* ML/Pure: generic Args/Attrib syntax everywhere;
2006-02-10, by wenzelm
moved fixedN to lexicon.ML;
2006-02-10, by wenzelm
added mfix_delims;
2006-02-10, by wenzelm
added mixfix_conflict;
2006-02-10, by wenzelm
added fixedN, constN;
2006-02-10, by wenzelm
tuned comment;
2006-02-10, by wenzelm
tuned comment;
2006-02-10, by wenzelm
syntax: Context.generic;
2006-02-10, by wenzelm
Context.generic is canonical state of parsers;
2006-02-10, by wenzelm
Local syntax depending on theory syntax.
2006-02-10, by wenzelm
decode: observe Syntax.constN;
2006-02-10, by wenzelm
removed obsolete add_typ/term_classes/tycons;
2006-02-10, by wenzelm
tuned extern_term, pretty_term';
2006-02-10, by wenzelm
removed set quick_and_dirty and ThmDeps.enable -- no effect here;
2006-02-10, by wenzelm
abbrevs: store in reverted orientation;
2006-02-10, by wenzelm
use proof_general.ML: setmp quick_and_dirty captures default value;
2006-02-10, by wenzelm
added Isar/local_syntax.ML;
2006-02-10, by wenzelm
tuned;
2006-02-10, by wenzelm
Args/Attrib syntax: Context.generic;
2006-02-10, by wenzelm
simplified polyml example;
2006-02-10, by wenzelm
tidying
2006-02-09, by paulson
blacklist tweaks
2006-02-09, by paulson
names for simprules
2006-02-09, by paulson
removed redundant lemmas
2006-02-09, by huffman
no longer need All_equiv lemmas
2006-02-09, by huffman
map_type_tvar/tfree: map_atyps;
2006-02-08, by wenzelm
tuned;
2006-02-08, by wenzelm
*** empty log message ***
2006-02-08, by nipkow
made "dvd" on numbers executable by simp.
2006-02-08, by nipkow
introduced gen_distinct in place of distinct
2006-02-08, by haftmann
fixed the most silly bug conceivable in map_atyps
2006-02-08, by haftmann
lambda: base name of Const;
2006-02-07, by wenzelm
adapted Sign.infer_types;
2006-02-07, by wenzelm
has_duplicates;
2006-02-07, by wenzelm
adapted Sign.infer_types;
2006-02-07, by wenzelm
added local consts component;
2006-02-07, by wenzelm
Library.is_equal;
2006-02-07, by wenzelm
removed obsolete sign_of_cterm;
2006-02-07, by wenzelm
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
2006-02-07, by wenzelm
export consts_of;
2006-02-07, by wenzelm
removed eq-polymorphic duplicates;
2006-02-07, by wenzelm
renamed space to space_of;
2006-02-07, by wenzelm
renamed gen_duplicates to duplicates;
2006-02-07, by wenzelm
slight improvements in code generation
2006-02-07, by haftmann
updated;
2006-02-06, by wenzelm
Logic.combound;
2006-02-06, by wenzelm
adapted Consts.dest;
2006-02-06, by wenzelm
Sign.cert_def;
2006-02-06, by wenzelm
added bound_vars;
2006-02-06, by wenzelm
TableFun: renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
Envir.(beta_)eta_contract;
2006-02-06, by wenzelm
added local_theory, with optional locale xname;
2006-02-06, by wenzelm
type local_theory;
2006-02-06, by wenzelm
norm_term: Sign.const_expansion, Envir.expand_atom;
2006-02-06, by wenzelm
TableFun: renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
type local_theory = Proof.context;
2006-02-06, by wenzelm
cert_def: use Logic.dest_def;
2006-02-06, by wenzelm
Toplevel.local_theory;
2006-02-06, by wenzelm
LocalDefs.cert_def;
2006-02-06, by wenzelm
eq_prop: Envir.beta_eta_contract;
2006-02-06, by wenzelm
renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
moved combound, rlist_abs to logic.ML;
2006-02-06, by wenzelm
union_tpairs: Library.merge;
2006-02-06, by wenzelm
moved no_vars to sign.ML;
2006-02-06, by wenzelm
lambda: abstract over any const;
2006-02-06, by wenzelm
added add_abbrevs(_i);
2006-02-06, by wenzelm
moved (beta_)eta_contract to envir.ML;
2006-02-06, by wenzelm
tuned;
2006-02-06, by wenzelm
added generic dest_def (mostly from theory.ML);
2006-02-06, by wenzelm
added (beta_)eta_contract (from pattern.ML);
2006-02-06, by wenzelm
print_theory: const abbreviations;
2006-02-06, by wenzelm
added abbreviations;
2006-02-06, by wenzelm
load envir.ML and logic.ML early;
2006-02-06, by wenzelm
Logic.rlist_abs;
2006-02-06, by wenzelm
Logic.const_of_class/class_of_const;
2006-02-06, by wenzelm
TableFun: renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
replaced Symtab.merge_multi by local merge_rules;
2006-02-06, by wenzelm
Envir.(beta_)eta_contract;
2006-02-06, by wenzelm
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-06, by haftmann
added strip_abs
2006-02-06, by haftmann
clarified semantics of merge
2006-02-06, by haftmann
speedup: use simproc for AC rules
2006-02-04, by huffman
UU_reorient_simproc no longer rewrites UU = numeral
2006-02-04, by huffman
removed obsolete gen_ins/mem;
2006-02-03, by wenzelm
removed add/del_rules;
2006-02-03, by wenzelm
canonical member/insert/merge;
2006-02-03, by wenzelm
removal of case analysis clauses
2006-02-03, by paulson
fix
2006-02-03, by haftmann
minor improvements
2006-02-03, by haftmann
refined signature of locale module
2006-02-03, by haftmann
no toplevel 'thy' anymore
2006-02-03, by haftmann
fix in codegen
2006-02-03, by haftmann
do not open structure;
2006-02-02, by wenzelm
reimplemented using Equiv_Relations.thy
2006-02-02, by huffman
improvement in devarifications
2006-02-02, by haftmann
alternative syntax for instances
2006-02-02, by haftmann
tuned;
2006-02-02, by wenzelm
consumes: negative argument relative to total number of prems;
2006-02-02, by wenzelm
added refine_insert;
2006-02-02, by wenzelm
Proof.refine_insert;
2006-02-02, by wenzelm
always use Attrib.src;
2006-02-02, by wenzelm
more generic type for map_specs/facts;
2006-02-02, by wenzelm
'obtains' element;
2006-02-02, by wenzelm
'obtain': optional case name;
2006-02-02, by wenzelm
index elements;
2006-02-02, by wenzelm
* Isar: 'obtains' element;
2006-02-02, by wenzelm
tuned msg;
2006-02-02, by wenzelm
theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02, by wenzelm
added parname;
2006-02-02, by wenzelm
obtain(_i): optional name for 'that';
2006-02-02, by wenzelm
tuned comments;
2006-02-02, by wenzelm
moved (general_)statement to outer_parse.ML;
2006-02-02, by wenzelm
added concluding statements: Shows/Obtains;
2006-02-02, by wenzelm
moved specific map_typ/term to sign.ML;
2006-02-02, by wenzelm
added specific map_typ/term (from term.ML);
2006-02-02, by wenzelm
Exporting recdef's hints for use by new recdef package
2006-02-02, by krauss
*_asms_of fixed.
2006-02-02, by ballarin
add 64bit atbroy98 platform
2006-02-02, by kleing
updated;
2006-02-01, by wenzelm
Added "evaluation" method and oracle.
2006-02-01, by berghofe
new and updated protocol proofs by Giamp Bella
2006-02-01, by paulson
substantial cleanup and simplifications
2006-02-01, by haftmann
name clarifications
2006-02-01, by haftmann
added map_entry_yield
2006-02-01, by haftmann
- renamed some lemmas (some had names coming from ancient
2006-02-01, by urbanc
added all constructors from PhD
2006-02-01, by urbanc
axiomatization: retrict parameters to occurrences in specs;
2006-01-31, by wenzelm
improved comments;
2006-01-31, by wenzelm
tuned LocalDefs.unfold;
2006-01-31, by wenzelm
(un)fold: removed '(raw)' option;
2006-01-31, by wenzelm
added consts_retricted;
2006-01-31, by wenzelm
(un)fold: no raw flag;
2006-01-31, by wenzelm
tuned;
2006-01-31, by wenzelm
tuned LocalTheory.pretty_consts;
2006-01-31, by wenzelm
(un)folded: removed '(raw)' option;
2006-01-31, by wenzelm
lambda: abstract over TYPE argument, too;
2006-01-31, by wenzelm
tuned comments;
2006-01-31, by wenzelm
removal of ResClause.num_of_clauses and other simplifications
2006-01-31, by paulson
working SPASS support; much tidying
2006-01-31, by paulson
added serialization for arbitrary
2006-01-31, by haftmann
minor change to CodegenPackage interface
2006-01-31, by haftmann
minor cleanups
2006-01-31, by haftmann
more coherent lookup extraction functions
2006-01-31, by haftmann
reorganization of code to support DFG otuput
2006-01-31, by paulson
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
2006-01-31, by wenzelm
declare defn rules;
2006-01-31, by wenzelm
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
2006-01-31, by wenzelm
export meta_rewrite_rule;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
tidy-up of res_clause.ML, removing the "predicates" field
2006-01-30, by paulson
'setup': no list type, support implicit setup;
2006-01-30, by wenzelm
'fixes': support plain vars;
2006-01-30, by wenzelm
fixed a syntax error!
2006-01-30, by paulson
replaced gen_list by enum
2006-01-30, by haftmann
adaptions to codegen_package
2006-01-30, by haftmann
various improvements
2006-01-30, by haftmann
added three times overloaded Isar instance command
2006-01-30, by haftmann
moved instance Isar command to class_package.ML
2006-01-30, by haftmann
added map_atype, map_aterms
2006-01-30, by haftmann
tuned proof;
2006-01-29, by wenzelm
declare atomize/defn for Ball;
2006-01-29, by wenzelm
invent_fixes: merely enter body temporarily;
2006-01-29, by wenzelm
'unfolding': LocalDefs.unfold;
2006-01-29, by wenzelm
moved treatment of object-logic equalities to local_defs.ML;
2006-01-29, by wenzelm
method (un)folded: option '(raw)';
2006-01-29, by wenzelm
added attributes defn_add/del;
2006-01-29, by wenzelm
added 'defn' attribute;
2006-01-29, by wenzelm
proper order of trfuns;
2006-01-29, by wenzelm
CPure: Context.add_setup;
2006-01-29, by wenzelm
tuned proofs;
2006-01-29, by wenzelm
implicit setup;
2006-01-29, by wenzelm
default rule step: norm_hhf_tac;
2006-01-29, by wenzelm
tuned comment;
2006-01-29, by wenzelm
declare 'defn' rules;
2006-01-29, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
Basic operations on local definitions.
2006-01-28, by wenzelm
removed unnecessary Syntax.fix_mixfix;
2006-01-28, by wenzelm
added axiomatization_loc, definition_loc;
2006-01-28, by wenzelm
moved local defs to local_defs.ML;
2006-01-28, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
removed unatomize;
2006-01-28, by wenzelm
(un)fold: support object-level rewrites;
2006-01-28, by wenzelm
added print_consts;
2006-01-28, by wenzelm
removed obsolete keyword 'files';
2006-01-28, by wenzelm
(un)folded: support object-level rewrites;
2006-01-28, by wenzelm
added equals_cong;
2006-01-28, by wenzelm
added Isar/local_defs.ML;
2006-01-28, by wenzelm
LocalDefs.add_def;
2006-01-28, by wenzelm
LocalDefs.def_export;
2006-01-28, by wenzelm
tuned proofs;
2006-01-28, by wenzelm
Pure/Isar: (un)folded, (un)fold, unfolding support
2006-01-28, by wenzelm
interrupt_timeout for Poly replaced by stub
2006-01-27, by webertj
added atomize_iff;
2006-01-27, by wenzelm
renamed Pretty.gen_list to Pretty.enum;
2006-01-27, by wenzelm
swapped theory_context;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
added invent_fixes;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
renamed reverse_atomize to unatomize;
2006-01-27, by wenzelm
init: include view;
2006-01-27, by wenzelm
improved 'notes', including proper treatment of locale results;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
Locale.init;
2006-01-27, by wenzelm
renamed gen_list to enum;
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
added ProofContext.pprint_context (depends on ProofContext.debug);
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
tidying up SPASS output
2006-01-27, by paulson
tidying
2006-01-27, by paulson
better reporting
2006-01-27, by paulson
Interface to access the specification of a named locale.
2006-01-27, by ballarin
Added new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Added in new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Changed codes that call relevance filter.
2006-01-27, by mengj
Relevance filtering. Has replaced the previous version.
2006-01-27, by mengj
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
2006-01-26, by webertj
smaller example to prevent timeout
2006-01-26, by webertj
Fixed bug in code generator for primitive definitions that
2006-01-26, by berghofe
Inductive sets with no introduction rules are now allowed as well.
2006-01-26, by berghofe
added definition(_i);
2006-01-25, by wenzelm
renamed export to export_standard (again!), because it includes Drule.local_standard';
2006-01-25, by wenzelm
ProofContext.export_standard;
2006-01-25, by wenzelm
tuned atomize_cterm;
2006-01-25, by wenzelm
turned abstract_term into ProofContext.abs_def;
2006-01-25, by wenzelm
added constant definition;
2006-01-25, by wenzelm
added 'definition';
2006-01-25, by wenzelm
tuned comment;
2006-01-25, by wenzelm
export name_multi;
2006-01-25, by wenzelm
abs_def: improved error;
2006-01-25, by wenzelm
ObjectLogic.atomize_cterm;
2006-01-25, by wenzelm
updated;
2006-01-25, by wenzelm
works with DPLL solver now
2006-01-24, by webertj
the additional freshness-condition in the one-induction
2006-01-24, by urbanc
fixed code_generate syntax;
2006-01-24, by wenzelm
renamed axiomatize(_i) to axiomatization(_i);
2006-01-24, by wenzelm
renamed inferred_type to inferred_param;
2006-01-24, by wenzelm
ProofContext.inferred_param;
2006-01-24, by wenzelm
removed the_params;
2006-01-24, by wenzelm
added actual operations;
2006-01-24, by wenzelm
axiomatization: optional vars;
2006-01-24, by wenzelm
LocalTheory.pretty_consts;
2006-01-24, by wenzelm
tuned;
2006-01-24, by wenzelm
add_finals: prep_consts, i.e. varify type;
2006-01-24, by wenzelm
added dest_all;
2006-01-24, by wenzelm
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
Updated to Isabelle 2006-01-23
2006-01-23, by krauss
made change for ex1
2006-01-23, by urbanc
removed problematic keyword 'atom'
2006-01-23, by haftmann
more general serializer
2006-01-23, by haftmann
slight steps forward
2006-01-23, by haftmann
exported after_qed for axclass instance
2006-01-23, by haftmann
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-23, by paulson
Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-23, by paulson
bugfix: induct_tac no longer raises THM "dest_state"
2006-01-23, by paulson
fixed the <<= notation
2006-01-23, by paulson
replacement of bool by a datatype (making problems first-order). More lemma names
2006-01-23, by paulson
Fixed a bug.
2006-01-23, by mengj
no essential changes
2006-01-22, by urbanc
made the change for setup-functions not returning functions
2006-01-22, by urbanc
a fixme comments about abs_fun_if, which should be called perm_if
2006-01-22, by urbanc
Local theory operations, with optional target locale.
2006-01-22, by wenzelm
added restore_body;
2006-01-22, by wenzelm
added the_params;
2006-01-22, by wenzelm
tuned order;
2006-01-22, by wenzelm
added Isar/local_theory.ML;
2006-01-22, by wenzelm
Ensure dereference is delayed.
2006-01-21, by mengj
tuned;
2006-01-21, by wenzelm
* ML: simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
removed duplicate type_solver (cf. Tools/typechk.ML);
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
rename map_theory/proof to theory/proof_map;
2006-01-21, by wenzelm
tuned proofs;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
type information is now also printed.
2006-01-20, by mengj
added some debugging code.
2006-01-20, by mengj
fixed a bug
2006-01-20, by mengj
quote "atom";
2006-01-19, by wenzelm
updated;
2006-01-19, by wenzelm
* ML/Isar: theory setup has type (theory -> theory);
2006-01-19, by wenzelm
use/use_thy: Output.toplevel_errors;
2006-01-19, by wenzelm
added basic syntax;
2006-01-19, by wenzelm
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
2006-01-19, by wenzelm
keep: disable Output.toplevel_errors;
2006-01-19, by wenzelm
run_thy: removed Output.toplevel_errors;
2006-01-19, by wenzelm
added ML_errors;
2006-01-19, by wenzelm
use: Output.ML_errors;
2006-01-19, by wenzelm
Syntax.basic_syn;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
tuned setmp;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
tuned comments;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
Use generic Simplifier.simp_add attribute instead
2006-01-19, by berghofe
Re-inserted consts_code declaration accidentally deleted
2006-01-19, by berghofe
strengthened some lemmas; simplified some proofs
2006-01-19, by paulson
substantial improvement in serialization handling
2006-01-18, by haftmann
fixed one proof that broke because of the changes
2006-01-18, by urbanc
substantial improvements in code generator
2006-01-17, by haftmann
these hacks are no longer needed
2006-01-17, by paulson
improved SPASS support
2006-01-17, by paulson
case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-16, by wenzelm
put_facts: do not pretend local thms were named;
2006-01-16, by wenzelm
declare the1_equality [elim?];
2006-01-16, by wenzelm
tuned;
2006-01-15, by wenzelm
tuned;
2006-01-15, by wenzelm
* Classical: optional weight for attributes;
2006-01-15, by wenzelm
guess: used fixed inferred_type of vars;
2006-01-15, by wenzelm
export add_args;
2006-01-15, by wenzelm
attributes: optional weight;
2006-01-15, by wenzelm
classical attributes: optional weight;
2006-01-15, by wenzelm
prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-15, by wenzelm
generic attributes;
2006-01-14, by wenzelm
tuned;
2006-01-14, by wenzelm
* ML/Isar: simplified treatment of user-level errors;
2006-01-14, by wenzelm
sane ERROR vs. TOPLEVEL_ERROR handling;
2006-01-14, by wenzelm
added Isar.toplevel;
2006-01-14, by wenzelm
Output.error_msg;
2006-01-14, by wenzelm
removed special ERROR handling stuff (transform_error etc.);
2006-01-14, by wenzelm
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
2006-01-14, by wenzelm
Output.debug;
2006-01-14, by wenzelm
generated code: raise Match instead of ERROR;
2006-01-14, by wenzelm
sane ERROR handling;
2006-01-14, by wenzelm
blacklist experiments
2006-01-13, by paulson
more readable divide ops
2006-01-13, by paulson
more practical time limit
2006-01-13, by paulson
*** empty log message ***
2006-01-13, by nipkow
mixfix: added Structure;
2006-01-13, by wenzelm
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
tuned;
2006-01-13, by wenzelm
generic_setup: optional argument, defaults to Context.setup();
2006-01-13, by wenzelm
added map_theory, map_proof;
2006-01-13, by wenzelm
removed obsolete sign_of;
2006-01-13, by wenzelm
implicit setup, which admits exception_trace;
2006-01-13, by wenzelm
ProofContext.def_export;
2006-01-13, by wenzelm
updated to new induction principle
2006-01-11, by urbanc
cahges to use the new induction-principle (now proved in
2006-01-11, by urbanc
changes to make use of the new induction principle proved by
2006-01-11, by urbanc
Implemented proof of (strong) induction rule.
2006-01-11, by berghofe
Added theorem at_finite_select.
2006-01-11, by berghofe
added lemmas perm_empty, perm_insert to do with
2006-01-11, by urbanc
merged the silly lemmas into the eqvt proof of subtype
2006-01-11, by urbanc
tuned proofs
2006-01-11, by urbanc
tuned the eqvt-proof
2006-01-11, by urbanc
rolled back the last addition since these lemmas were already
2006-01-11, by urbanc
added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)
2006-01-11, by urbanc
tuned
2006-01-11, by urbanc
tidied, and added missing thm divide_less_eq_1_neg
2006-01-11, by paulson
tidied, and giving theorems names
2006-01-11, by paulson
add transitivity rules
2006-01-11, by huffman
tuned;
2006-01-11, by wenzelm
updated;
2006-01-11, by wenzelm
tuned;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
* ML: generic context, data, attributes;
2006-01-10, by wenzelm
added context_of -- generic context;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
print rules: generic context;
2006-01-10, by wenzelm
Specification.pretty_consts ctxt;
2006-01-10, by wenzelm
generic data and attributes;
2006-01-10, by wenzelm
added rule, declaration;
2006-01-10, by wenzelm
added generic syntax;
2006-01-10, by wenzelm
tuned dependencies;
2006-01-10, by wenzelm
added declaration_attribute;
2006-01-10, by wenzelm
support for generic contexts with data;
2006-01-10, by wenzelm
fix_tac: no warning;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
Attrib.rule;
2006-01-10, by wenzelm
tuned
2006-01-10, by urbanc
added the lemmas supp_char and supp_string
2006-01-10, by urbanc
added some lemmas to the collection "abs_fresh"
2006-01-09, by urbanc
_E suffix for compatibility with AddIffs
2006-01-09, by paulson
tidied
2006-01-09, by paulson
simplified the special-case simprules
2006-01-09, by paulson
theorems need names
2006-01-09, by paulson
commented the transitivity and narrowing proof
2006-01-09, by urbanc
Theory specifications --- with type-inference, but no internal polymorphism.
2006-01-07, by wenzelm
added infer_type, declared_type;
2006-01-07, by wenzelm
added param, spec, named_spec;
2006-01-07, by wenzelm
added init;
2006-01-07, by wenzelm
added 'axiomatization';
2006-01-07, by wenzelm
Specification.pretty_consts;
2006-01-07, by wenzelm
gen_names: preserve empty names;
2006-01-07, by wenzelm
added Isar/specification.ML;
2006-01-07, by wenzelm
updated;
2006-01-07, by wenzelm
another change for the new induct-method
2006-01-07, by urbanc
RuleCases.make_nested;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
RuleCases.make_common;
2006-01-07, by wenzelm
pretty_locale: backquote notes;
2006-01-07, by wenzelm
RuleCases.make_simple;
2006-01-07, by wenzelm
tuned order;
2006-01-07, by wenzelm
added backquote;
2006-01-07, by wenzelm
RuleCases.make_common/nested;
2006-01-07, by wenzelm
* Provers/induct: improved simultaneous goals -- nested cases;
2006-01-07, by wenzelm
added private datatype nprod (copy of prod) to be
2006-01-07, by urbanc
changed PRO_RED proof to conform with the new induction rules
2006-01-07, by urbanc
prep_meta_eq: reuse mk_rews of local simpset;
2006-01-06, by wenzelm
removed obsolete eqrule_HOL_data.ML;
2006-01-06, by wenzelm
removed obsolete eqrule_FOL_data.ML;
2006-01-06, by wenzelm
simplified EqSubst setup;
2006-01-06, by wenzelm
obsolete, reuse mk_rews of local simpset;
2006-01-06, by wenzelm
Toplevel.theory_to_proof;
2006-01-06, by wenzelm
transactions now always see quasi-functional intermediate checkpoint;
2006-01-06, by wenzelm
tuned EqSubst setup;
2006-01-06, by wenzelm
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-06, by wenzelm
hide type datatype node;
2006-01-05, by wenzelm
tuned print_theorems_theory;
2006-01-05, by wenzelm
Toplevel.proof_position_of;
2006-01-05, by wenzelm
store_thm: transfer to current context, i.e. the target theory;
2006-01-05, by wenzelm
replaced swap by contrapos_np;
2006-01-05, by wenzelm
added setminus;
2006-01-05, by wenzelm
proper handling of simultaneous goals and mutual rules;
2006-01-05, by wenzelm
provide projections of induct_weak, induct_unsafe;
2006-01-05, by wenzelm
added strict_mutual_rule;
2006-01-05, by wenzelm
RuleCases.strict_mutual_rule;
2006-01-05, by wenzelm
changed the name of the type "nOption" to "noption".
2006-01-05, by urbanc
added "fresh_singleton" lemma
2006-01-04, by urbanc
added more documentation; will now try out a modification
2006-01-04, by urbanc
Reversed Larry's option/iff change.
2006-01-04, by nipkow
substantial additions using locales
2006-01-04, by haftmann
exported read|cert_arity interfaces
2006-01-04, by haftmann
trace_simp_depth_limit is 1 by default
2006-01-04, by nipkow
removed pointless trace msg.
2006-01-04, by nipkow
preservation of names
2006-01-04, by paulson
a few more named lemmas
2006-01-04, by paulson
fix: reintroduced pred_ctxt in gen_add_locale
2006-01-04, by haftmann
tuned;
2006-01-04, by wenzelm
* Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-04, by wenzelm
added unlocalize_mfix;
2006-01-04, by wenzelm
added unlocalize_mixfix;
2006-01-04, by wenzelm
added theory_to_theory_to_proof, which may change theory before entering the proof;
2006-01-04, by wenzelm
tuned;
2006-01-04, by wenzelm
moved forget_proof to toplevel.ML;
2006-01-04, by wenzelm
Toplevel.forget_proof;
2006-01-04, by wenzelm
adapted Toplevel.Proof;
2006-01-04, by wenzelm
removed dead code;
2006-01-04, by wenzelm
more stuff;
2006-01-04, by wenzelm
Provers/classical: stricter checks to ensure that supplied intro, dest and
2006-01-03, by paulson
added explicit paths to required theories
2006-01-03, by paulson
added implementation manual;
2006-01-03, by wenzelm
more stuff;
2006-01-03, by wenzelm
fixed LaTeX source;
2006-01-03, by wenzelm
class now a keyword
2006-01-03, by haftmann
class now an keyword, quoted where necessary
2006-01-03, by haftmann
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
2006-01-03, by haftmann
rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03, by haftmann
added unfolding(_i);
2006-01-03, by wenzelm
unparse String/AltString: escape quotes;
2006-01-03, by wenzelm
tuned;
2006-01-03, by wenzelm
avoid hardwired Trueprop;
2006-01-03, by wenzelm
added 'using' command;
2006-01-03, by wenzelm
updated;
2006-01-03, by wenzelm
added IsarImplementation;
2006-01-03, by wenzelm
updated -- lost update!?
2006-01-03, by wenzelm
* Pure/Isar: new command 'unfolding';
2006-01-03, by wenzelm
ISABELLE_USER for remote cvs access;
2006-01-02, by wenzelm
outline;
2006-01-02, by wenzelm
"The Isabelle/Isar Implementation" manual;
2006-01-02, by wenzelm
* Provers/classical: removed obsolete classical version of elim_format;
2005-12-31, by wenzelm
tuned forall_intr_vars;
2005-12-31, by wenzelm
added classical_rule, which replaces Data.make_elim;
2005-12-31, by wenzelm
explicitly reject consts *Goal*, *False*;
2005-12-31, by wenzelm
elim rules: Classical.classical_rule;
2005-12-31, by wenzelm
removed obsolete cla_dist_concl;
2005-12-31, by wenzelm
removed classical elim_format;
2005-12-31, by wenzelm
removed obsolete Provers/make_elim.ML;
2005-12-31, by wenzelm
obsolete, see classical_rule in Provers/classical.ML;
2005-12-31, by wenzelm
more robust phantomsection;
2005-12-31, by wenzelm
require cla_dist_concl, avoid assumptions about concrete syntax;
2005-12-30, by wenzelm
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
2005-12-30, by wenzelm
provide equality_name, not_name;
2005-12-30, by wenzelm
fixed final_consts;
2005-12-30, by wenzelm
provide cla_dist_concl;
2005-12-30, by wenzelm
non-PDF: phantomsection;
2005-12-30, by wenzelm
added atom keyword
2005-12-29, by haftmann
changes in code generator keywords
2005-12-29, by haftmann
adaptions to changes in code generator
2005-12-29, by haftmann
slight improvements
2005-12-29, by haftmann
slightly improved serialization
2005-12-28, by haftmann
substantial improvements in code generating
2005-12-27, by haftmann
added map_index
2005-12-27, by haftmann
tuned proofs;
2005-12-23, by wenzelm
removed obsolete atomize_old;
2005-12-23, by wenzelm
removed obsolete induct_atomize_old;
2005-12-23, by wenzelm
the "skolem" attribute and better initialization of the clause database
2005-12-23, by paulson
blacklist of prolific theorems (must be replaced by an attribute later
2005-12-23, by paulson
tidied
2005-12-23, by paulson
tuned;
2005-12-23, by wenzelm
* Provers/induct: support simultaneous goals with mutual rules;
2005-12-23, by wenzelm
induct etc.: admit multiple rules;
2005-12-23, by wenzelm
backpatching of Substring.full;
2005-12-23, by wenzelm
goal/qed: proper treatment of two levels of conjunctions;
2005-12-23, by wenzelm
Logic.mk_conjunction_list;
2005-12-23, by wenzelm
turned bicompose_no_flatten into compose_no_flatten, without elimination;
2005-12-23, by wenzelm
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
2005-12-23, by wenzelm
added mk_conjunction_list2;
2005-12-23, by wenzelm
conj_elim_precise: proper treatment of nested conjunctions;
2005-12-23, by wenzelm
Thm.compose_no_flatten;
2005-12-23, by wenzelm
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
2005-12-23, by wenzelm
is_prefix
2005-12-23, by haftmann
slight improvements
2005-12-22, by haftmann
more lemmas
2005-12-22, by nipkow
shorter proof
2005-12-22, by paulson
Tuned syntax for perm.
2005-12-22, by berghofe
new lemmas
2005-12-22, by nipkow
Fixed a use of an outdated Substring function
2005-12-22, by paulson
tuned;
2005-12-22, by wenzelm
exh_casedist2: norm_hhf_eq;
2005-12-22, by wenzelm
added bicompose_no_flatten, which refrains from
2005-12-22, by wenzelm
bicompose_proof: no_flatten;
2005-12-22, by wenzelm
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
2005-12-22, by wenzelm
Transform mutual rule into projection.
2005-12-22, by wenzelm
added Provers/project_rule.ML
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
* induct: improved treatment of mutual goals and mutual rules;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
prop_tr': proper handling of aprop marked as bound;
2005-12-22, by wenzelm
consume: expand defs in prems of concls;
2005-12-22, by wenzelm
cases: main is_proper flag;
2005-12-22, by wenzelm
auto cases: marked improper;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
CONJUNCTS2;
2005-12-22, by wenzelm
rule_context: numbered cases;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
renamed imp_cong' to imp_cong_rule;
2005-12-22, by wenzelm
mk_conjunction: proper treatment of bounds;
2005-12-22, by wenzelm
fixed has_internal;
2005-12-22, by wenzelm
Tactic.precise_conjunction_tac;
2005-12-22, by wenzelm
added locale meta_conjunction_syntax and various conjunction rules;
2005-12-22, by wenzelm
simplified setup: removed dest_concls, local_impI, conjI;
2005-12-22, by wenzelm
induct_rulify;
2005-12-22, by wenzelm
actually produce projected rules;
2005-12-22, by wenzelm
*.inducts holds all projected rules;
2005-12-22, by wenzelm
tuned;
2005-12-22, by wenzelm
tuned induct proofs;
2005-12-22, by wenzelm
mutual induct with *.inducts;
2005-12-22, by wenzelm
wf_induct_rule: consumes 1;
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
slight improvements
2005-12-21, by haftmann
slight improvements in name handling
2005-12-21, by haftmann
slight refinements
2005-12-21, by haftmann
added eq_ord
2005-12-21, by haftmann
slight clean ups
2005-12-21, by haftmann
discontinued unflat in favour of burrow and burrow_split
2005-12-21, by haftmann
new hash table module in HOL/Too/s
2005-12-21, by paulson
modified suffix for [iff] attribute
2005-12-21, by paulson
removed or modified some instances of [iff]
2005-12-21, by paulson
tuned;
2005-12-20, by wenzelm
added .cvsignore
2005-12-20, by haftmann
removed improper .cvsignore
2005-12-20, by haftmann
removed superfluos is_prefix functions
2005-12-20, by haftmann
resolved shadowing of Library.find_first
2005-12-20, by haftmann
removed infix prefix, introduces burrow
2005-12-20, by haftmann
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-20, by mengj
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-20, by mengj
made the changes according to Florian's re-arranging of
2005-12-19, by urbanc
added proofs to show that every atom-kind combination
2005-12-19, by urbanc
added thms to perm_compose (so far only composition
2005-12-19, by urbanc
tuned one comment
2005-12-19, by urbanc
fixed a bug that occured when more than one atom-type
2005-12-19, by urbanc
fixed proof
2005-12-19, by nipkow
more cleaning up - this time of the cp-instance
2005-12-18, by urbanc
improved the finite-support proof
2005-12-18, by urbanc
improved the code for showing that a type is
2005-12-18, by urbanc
simp del: empty_Collect_eq;
2005-12-17, by wenzelm
sort_distinct;
2005-12-17, by wenzelm
added sort_distinct;
2005-12-17, by wenzelm
added container-lemma fresh_eqvt
2005-12-16, by urbanc
I think the earlier version was completely broken
2005-12-16, by urbanc
tuned more proofs
2005-12-16, by urbanc
new lemmas
2005-12-16, by nipkow
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
hashing to eliminate the output of duplicate clauses
2005-12-16, by paulson
hash tables from SML/NJ
2005-12-16, by paulson
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
there was a small error in the last commit - fixed now
2005-12-15, by urbanc
tuned more proof and added in-file documentation
2005-12-15, by urbanc
improved proofs;
2005-12-15, by wenzelm
acc_induct: proper tags;
2005-12-15, by wenzelm
removed obsolete/unused setup_induction;
2005-12-15, by wenzelm
tuned the proof of transitivity/narrowing
2005-12-15, by urbanc
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
2005-12-15, by paulson
made further tunings
2005-12-15, by urbanc
Added functions to test equivalence between clauses.
2005-12-15, by mengj
ex/Sudoku.thy
2005-12-14, by webertj
deleted redundant (looping!) simprule
2005-12-14, by paulson
modified example for new clauses
2005-12-14, by paulson
removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-14, by paulson
removed unused function repeat_RS
2005-12-14, by paulson
Changed literals' ordering and the functions for sorting literals.
2005-12-14, by mengj
1. changed fol_type, it's not a string type anymore.
2005-12-14, by mengj
changed ATP input files' names and location.
2005-12-14, by mengj
Potentially infinite lists as greatest fixed-point.
2005-12-13, by wenzelm
Provers/induct: coinduct;
2005-12-13, by wenzelm
tuned proofs;
2005-12-13, by wenzelm
added HOL/Library/Coinductive_List.thy;
2005-12-13, by wenzelm
added a fresh_left lemma that contains all instantiation
2005-12-13, by urbanc
initial commit (not to be seen by the public)
2005-12-13, by urbanc
simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-13, by chaieb
deals with Suc in mod expressions
2005-12-13, by chaieb
Poplog/pml provides a proper print function already!
2005-12-13, by wenzelm
meson no longer does these examples
2005-12-13, by paulson
now generates the name "append"
2005-12-13, by paulson
removal of functional reflexivity axioms
2005-12-13, by paulson
list_of_indset now also generates code for set type.
2005-12-13, by berghofe
added generic name mangler
2005-12-12, by haftmann
improvement in eq handling
2005-12-12, by haftmann
improvements in class and eq handling
2005-12-12, by haftmann
added dummy 'print' to non-polyml systems
2005-12-12, by haftmann
ISAR-fied some proofs
2005-12-11, by urbanc
completed the sn proof and changed the manual
2005-12-11, by urbanc
changed the types in accordance with Florian's changes
2005-12-10, by urbanc
substantial improvements for class code generation
2005-12-09, by haftmann
improved extraction interface
2005-12-09, by haftmann
tuned
2005-12-09, by urbanc
oriented result pairs in PureThy
2005-12-09, by haftmann
tuned;
2005-12-08, by wenzelm
removed Syntax.deskolem;
2005-12-08, by wenzelm
swap: no longer pervasive;
2005-12-08, by wenzelm
replaced swap by contrapos_np;
2005-12-08, by wenzelm
tuned proofs;
2005-12-08, by wenzelm
Cla.swap;
2005-12-08, by wenzelm
removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08, by wenzelm
tuned sources and proofs
2005-12-08, by wenzelm
Classical.swap;
2005-12-08, by wenzelm
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-12-08, by wenzelm
Adapted to new type of PureThy.add_defs_i.
2005-12-08, by berghofe
replaced swap by Classical.swap;
2005-12-07, by wenzelm
avoid unportable tail;
2005-12-07, by wenzelm
tuned
2005-12-07, by urbanc
removed thms 'swap' and 'nth_map' from ML toplevel
2005-12-06, by haftmann
improved serialization of classes to haskell
2005-12-06, by haftmann
improved class handling
2005-12-06, by haftmann
added 'dig' combinator
2005-12-06, by haftmann
re-oriented some result tuples in PureThy
2005-12-06, by haftmann
Added more functions for new type embedding of HOL clauses.
2005-12-06, by mengj
Added new type embedding methods for translating HOL clauses.
2005-12-06, by mengj
added code to say that discrete types (nat, bool, char)
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
transitivity should be now in a reasonable state. But
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
ISAR-fied two proofs
2005-12-05, by urbanc
Adapted to new type of store_thmss(_atts).
2005-12-05, by berghofe
Added store_thmss_atts to signature again.
2005-12-05, by berghofe
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
added an Isar-proof for the abs_ALL lemma
2005-12-04, by urbanc
tuning
2005-12-04, by urbanc
defines: beta/eta contract lhs;
2005-12-02, by wenzelm
asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-12-02, by wenzelm
mixfix_args: 1 for binders;
2005-12-02, by wenzelm
removed fixed_tr: now handled in syntax module;
2005-12-02, by wenzelm
added mixfixT;
2005-12-02, by wenzelm
defs: beta/eta contract lhs;
2005-12-02, by wenzelm
abs_def: beta/eta contract lhs;
2005-12-02, by wenzelm
Added recdef congruence rules for bounded quantifiers and commonly used
2005-12-02, by krauss
various improvements
2005-12-02, by haftmann
adjusted to improved code generator interface
2005-12-02, by haftmann
added perhaps option combinator
2005-12-02, by haftmann
adopted keyword for code generator
2005-12-02, by haftmann
Factored out proof for normalization of applications (norm_list).
2005-12-02, by berghofe
introduced new map2, fold
2005-12-02, by haftmann
typo
2005-12-01, by kleing
simprocs: static evaluation of simpset;
2005-12-01, by wenzelm
tuned;
2005-12-01, by wenzelm
tuned msg;
2005-12-01, by wenzelm
ProofContext.lthms_containing: suppress obvious duplicates;
2005-12-01, by wenzelm
unfold_tac: static evaluation of simpset;
2005-12-01, by wenzelm
superceded by timestart|stop.bash;
2005-12-01, by wenzelm
cpu time = user + system;
2005-12-01, by wenzelm
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
2005-12-01, by wenzelm
assoc_consts and assoc_types now check number of arguments in template.
2005-12-01, by berghofe
Added new component "sorts" to record datatype_info.
2005-12-01, by berghofe
timestop - report timing based on environment (cf. timestart.bash);
2005-12-01, by wenzelm
timestart - setup bash environment for timing;
2005-12-01, by wenzelm
Improved norm_proof to handle proofs containing term (type) variables
2005-12-01, by berghofe
restoring the old status of subset_refl
2005-12-01, by paulson
oriented pairs theory * 'a to 'a * theory
2005-12-01, by haftmann
initial cleanup to use the new induction method
2005-12-01, by urbanc
cleaned up further the proofs (diamond still needs work);
2005-12-01, by urbanc
changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-12-01, by urbanc
match_bind(_i): return terms;
2005-11-30, by wenzelm
method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-30, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip