isabelle: Graph

simplified definitions of flift1, flift2, liftpair;
2005-07-05, by huffman
tuned K;
2005-07-05, by wenzelm
fixed regexp grouping;
2005-07-05, by wenzelm
List.app;
2005-07-05, by wenzelm
added combinatros '||>' and '||>>' and fold_map fitting nicely to ST combinator '|->'
2005-07-05, by haftmann
tuned;
2005-07-05, by wenzelm
* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
2005-07-05, by wenzelm
added ST combinator '|->'
2005-07-05, by haftmann
Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;
2005-07-05, by wenzelm
tuned;
2005-07-05, by wenzelm
made smlnj happy;
2005-07-04, by wenzelm
methods: added simp_flags argument, added "depth_limit" flag;
2005-07-04, by wenzelm
added transform_exceptions: bool ref;
2005-07-04, by wenzelm
tuned;
2005-07-04, by wenzelm
dummy exception_trace;
2005-07-04, by wenzelm
tuned union: avoid garbage in trivial case;
2005-07-04, by wenzelm
dest_ctyp: raise exception for non-constructor;
2005-07-04, by wenzelm
added fast_indexname_ord, fast_term_ord;
2005-07-04, by wenzelm
use fast_string_ord;
2005-07-04, by wenzelm
added fast_string_ord;
2005-07-04, by wenzelm
Streamlined the signal handler in watcher.ML
2005-07-04, by quigley
unified main and dist
2005-07-04, by haftmann
started unifying main and dist
2005-07-04, by haftmann
(intermediate commit)
2005-07-04, by haftmann
Simple report generator for Poly/ML profiling output.
2005-07-02, by wenzelm
tuned;
2005-07-01, by wenzelm
ambig msg: warning again;
2005-07-01, by wenzelm
avoid polyeq;
2005-07-01, by wenzelm
tuned term_ord: less garbage;
2005-07-01, by wenzelm
cterm_aconv: avoid rep_cterm;
2005-07-01, by wenzelm
decomp_simp: compare terms, not cterms;
2005-07-01, by wenzelm
back to 1.28;
2005-07-01, by wenzelm
prime is a predicate now.
2005-07-01, by nipkow
* Isar profiling: new reference Toplevel.profiling (default 0);
2005-07-01, by wenzelm
use tracing for potentially voluminous ambiguity output;
2005-07-01, by wenzelm
added profiler interface (dummy);
2005-07-01, by wenzelm
added profiler interface, keep 'profiling' of PolyML structure;
2005-07-01, by wenzelm
added profile flag;
2005-07-01, by wenzelm
low-level tuning of map, fold;
2005-07-01, by wenzelm
ctyp: added 'sorts' field;
2005-07-01, by wenzelm
added all_sorts_nonempty;
2005-07-01, by wenzelm
low-level tuning of fold, fold_rev, foldl_map;
2005-07-01, by wenzelm
isatool install: removed KDE option;
2005-07-01, by wenzelm
Fixed bug: lookup' must use = instead of eq_type to compare types of
2005-07-01, by berghofe
Changed interface of Envir.lookup'
2005-07-01, by berghofe
Moved eq_type from envir.ML to type.ML
2005-07-01, by berghofe
Implemented modular code generation.
2005-07-01, by berghofe
Simplified proof (thanks to strengthened ball_cong).
2005-07-01, by berghofe
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
2005-07-01, by berghofe
Adapted to new interface of RecfunCodegen.add.
2005-07-01, by berghofe
Adapted to modular code generation.
2005-07-01, by berghofe
Corrected implementation of arbitrary on cname.
2005-07-01, by berghofe
Added BasisLibrary prefix to List.concat to avoid problems with
2005-07-01, by berghofe
Moved code generator setup from NatBin to IntDef.
2005-07-01, by berghofe
Simplified some proofs (thanks to strong_setsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack (thanks to strong_setsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack (thanks to strengthened finsum_cong).
2005-07-01, by berghofe
Removed setsubgoaler hack.
2005-07-01, by berghofe
Tuned finsum_cong to allow that premises are simplified more eagerly.
2005-07-01, by berghofe
Added strong_ball_cong and strong_bex_cong (these are now the standard
2005-07-01, by berghofe
Moved some code lemmas from Main to Nat.
2005-07-01, by berghofe
Adapted to new interface of code generator.
2005-07-01, by berghofe
Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
2005-07-01, by berghofe
Added strong_setsum_cong and strong_setprod_cong.
2005-07-01, by berghofe
defaultsort pcpo
2005-07-01, by huffman
added theorem lift_definedE; moved cont_if to Cont.thy
2005-07-01, by huffman
added tactic cont_tac
2005-07-01, by huffman
remove uses of sign_of
2005-07-01, by huffman
cleaned up
2005-07-01, by huffman
cleaned up
2005-07-01, by huffman
renamed flatdom2monofun to flatdom_strict2mono
2005-07-01, by huffman
cleaned up; reorganized and added section headings
2005-07-01, by huffman
cleaned up; added adm_less to adm_lemmas; added subsection headings
2005-07-01, by huffman
revert to 1.27 due to obscure performance issues (!??);
2005-06-30, by wenzelm
replace filter2 with List.partition
2005-06-30, by huffman
Proper treatment of beta-redexes in witness theorems.
2005-06-30, by ballarin
minor corrections
2005-06-30, by haftmann
test sml-dev on mac as well
2005-06-30, by kleing
use only 1 CPU on MacOS 10.4.1
2005-06-30, by kleing
use kleing@cse instead of kleing@in.tum.de
2005-06-30, by kleing
use global settings for isatest-doc
2005-06-30, by kleing
export no_type_brackets;
2005-06-29, by wenzelm
proper treatment of advanced trfuns: pass thy argument;
2005-06-29, by wenzelm
transform_failure in translation functions: TRANSLATION_FAIL;
2005-06-29, by wenzelm
proper treatment of advanced trfuns: pass thy argument;
2005-06-29, by wenzelm
accomodate advanced trfuns;
2005-06-29, by wenzelm
removed obsolete (un)fold_ast2;
2005-06-29, by wenzelm
Drule.implies_intr_hyps;
2005-06-29, by wenzelm
added print': print depending on print_mode;
2005-06-29, by wenzelm
no Syntax.internal on thesis;
2005-06-29, by wenzelm
added print_mode three_buffersN and corresponding cond_print;
2005-06-29, by wenzelm
cond_print for end-of-proof and calculational commands;
2005-06-29, by wenzelm
added eq;
2005-06-29, by wenzelm
pass thy as explicit argument (the old ref was not safe
2005-06-29, by wenzelm
more efficient treatment of shyps and hyps (use ordered lists);
2005-06-29, by wenzelm
Syntax.read thy;
2005-06-29, by wenzelm
tuned sort_ord: pointer_eq;
2005-06-29, by wenzelm
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
2005-06-29, by wenzelm
eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
2005-06-29, by wenzelm
replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
2005-06-29, by wenzelm
added implies_intr_hyps (from thm.ML);
2005-06-29, by wenzelm
added joinable;
2005-06-29, by wenzelm
stylistic improvements
2005-06-28, by paulson
added project information in overview
2005-06-28, by haftmann
added project information in overview
2005-06-28, by haftmann
more sophisticated pypager
2005-06-28, by haftmann
first-order check now allows quantifiers
2005-06-28, by paulson
stricter first-order check for meson
2005-06-28, by paulson
Constant "If" is now local
2005-06-28, by paulson
more sophisticated pypager
2005-06-28, by haftmann
replacing zabs_def by abs_if
2005-06-28, by paulson
introduced a notion of mirrors
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
some minor improvements
2005-06-28, by haftmann
corrected comment
2005-06-28, by haftmann
some corrections
2005-06-28, by haftmann
export get_calculation;
2005-06-26, by wenzelm
Added term_lpo
2005-06-25, by nipkow
cancels completely within terms as well now.
2005-06-25, by nipkow
Changes due to new abel_cancel.ML
2005-06-25, by nipkow
use both processors on macbroy5
2005-06-25, by kleing
switch mac test to macbroy5
2005-06-25, by kleing
cleaned up
2005-06-25, by huffman
cleaned up proof of contlub_abstraction
2005-06-25, by huffman
meson method taking an argument list
2005-06-24, by paulson
deleted a redundant "use" line
2005-06-24, by paulson
tidying
2005-06-24, by paulson
stylistic tweaks concerning Find
2005-06-24, by paulson
shortened time out by 3h (gives up at 12:00h now).
2005-06-24, by kleing
made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts,
2005-06-24, by kleing
needed for Isabelle independent build
2005-06-24, by kleing
added theorems fix_strict, fix_defined, fix_id, fix_const
2005-06-23, by huffman
add binder syntax for flift1
2005-06-23, by huffman
add new file to test fixrec package
2005-06-23, by huffman
add csplit3, ssplit3, fup3 as simp rules
2005-06-23, by huffman
New features:
2005-06-23, by huffman
added match functions for spair, sinl, sinr
2005-06-23, by huffman
fixed \<Prod> syntax
2005-06-23, by nipkow
new
2005-06-23, by nipkow
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
2005-06-22, by quigley
* Pure: the Isar proof context type is already defined early in Pure
2005-06-22, by wenzelm
added find2
2005-06-22, by nipkow
*** empty log message ***
2005-06-22, by nipkow
tunes Find
2005-06-22, by nipkow
added Rules/find2
2005-06-22, by nipkow
tuned pointer_eq;
2005-06-22, by wenzelm
renamed data kind;
2005-06-22, by wenzelm
removed proof data (see Pure/context.ML);
2005-06-22, by wenzelm
added depth_of;
2005-06-22, by wenzelm
removed obsolete object.ML (see Pure/library.ML);
2005-06-22, by wenzelm
export sort_ord;
2005-06-22, by wenzelm
renamed init to init_data;
2005-06-22, by wenzelm
added structure Object (from Pure/General/object.ML);
2005-06-22, by wenzelm
tuned;
2005-06-22, by wenzelm
begin_thy: merge maximal imports;
2005-06-22, by wenzelm
removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
2005-06-22, by wenzelm
improved proof;
2005-06-22, by wenzelm
obsolete (see Pure/context.ML);
2005-06-22, by wenzelm
tuned;
2005-06-22, by wenzelm
pointer equality for sml/nj
2005-06-22, by paulson
(initial commit)
2005-06-22, by haftmann
(initial commit)
2005-06-22, by haftmann
(initial commit)
2005-06-22, by haftmann
(initial commit)
2005-06-22, by haftmann
*** empty log message ***
2005-06-22, by nipkow
tuned
2005-06-22, by nipkow
added -H false
2005-06-22, by nipkow
Integrated vampire lemma code.
2005-06-21, by quigley
*** empty log message ***
2005-06-21, by nipkow
added find thms section
2005-06-21, by nipkow
proper implementation of pointer_eq;
2005-06-21, by wenzelm
tuned pointer_eq;
2005-06-21, by wenzelm
VAMPIRE_HOME, helper_path and various stylistic tweaks
2005-06-21, by paulson
lemma, equation between rtrancl and trancl
2005-06-21, by kleing
enter_thms: use theorem database of thy *after* attribute application;
2005-06-21, by wenzelm
tuned;
2005-06-21, by wenzelm
added subset, eq_set;
2005-06-21, by wenzelm
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
2005-06-21, by wenzelm
fixed HOL-Complex-Matrix target;
2005-06-21, by wenzelm
removed mkcontent from makedist
2005-06-21, by haftmann
fix 'give up waiting message' (logs of running processes are not attached)
2005-06-21, by kleing
* Pure: get_thm interface expects datatype thmref;
2005-06-20, by wenzelm
avoid identifier 'Name';
2005-06-20, by wenzelm
Theory.begin/end_theory;
2005-06-20, by wenzelm
clarify empty vs. pure browser info;
2005-06-20, by wenzelm
added pointer_eq;
2005-06-20, by wenzelm
thmref: Name vs. NameSelection;
2005-06-20, by wenzelm
refl_tac: avoid failure of unification, i.e. confusing trace msg;
2005-06-20, by wenzelm
print_theorems: proper use of PureThy.print_theorems_diff;
2005-06-20, by wenzelm
thmref: Name vs. NameSelection;
2005-06-20, by wenzelm
generalized type of inter;
2005-06-20, by wenzelm
added previous;
2005-06-20, by wenzelm
added begin_theory, end_theory;
2005-06-20, by wenzelm
added certify_prop, cert_term, cert_prop;
2005-06-20, by wenzelm
datatype thmref = Name ... | NameSelection ...;
2005-06-20, by wenzelm
added member, option_ord;
2005-06-20, by wenzelm
OrdList.inter;
2005-06-20, by wenzelm
tuned;
2005-06-20, by wenzelm
improved treatment of intermediate checkpoints: actual copy
2005-06-20, by wenzelm
added add_fixrec_i, add_fixpat_i;
2005-06-20, by wenzelm
proper header;
2005-06-20, by wenzelm
get_thm(s): Name;
2005-06-20, by wenzelm
get_thm instead of obsolete Goals.get_thm;
2005-06-20, by wenzelm
HOL-Matrix: plain session;
2005-06-20, by wenzelm
removed obsolete print_depth;
2005-06-20, by wenzelm
be less ambitious about the author's name;
2005-06-20, by wenzelm
exclude pghead.pdf from doc;
2005-06-20, by wenzelm
improved formatting;
2005-06-20, by wenzelm
use Tools/ATP/VampCommunication.ML;
2005-06-20, by wenzelm
Added VampCommunication.ML.
2005-06-20, by quigley
moved configure to lib/scripts;
2005-06-20, by wenzelm
./configure obsolete on virtually all systems, but apt to cause problems;
2005-06-20, by wenzelm
using TPTP2X_HOME; indentation, etc
2005-06-20, by paulson
fixed a faulty proof
2005-06-20, by paulson
moving some generic inequalities from integer arith to nat arith
2005-06-20, by paulson
(moved to Distribution/lib/scripts)
2005-06-20, by haftmann
added fixheaders
2005-06-20, by haftmann
improved comment;
2005-06-19, by wenzelm
some minor adaptions to make it work again;
2005-06-19, by wenzelm
tuned;
2005-06-18, by wenzelm
tuned remove;
2005-06-18, by wenzelm
added member;
2005-06-18, by wenzelm
added Pure/General/ord_list.ML;
2005-06-18, by wenzelm
Ordered lists without duplicates.
2005-06-18, by wenzelm
fixrec shows unsolved subgoals when proofs of rewrites fail
2005-06-18, by huffman
make match_rews into simp rules by default
2005-06-18, by huffman
support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
2005-06-17, by huffman
added match functions for ONE, TT, and FF; added theorem mplus_fail2
2005-06-17, by huffman
updated;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
Context.names_of;
2005-06-17, by wenzelm
* Pure/TheoryDataFun: change of the argument structure;
2005-06-17, by wenzelm