isabelle: Graph

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
Sign.root_path, Sign.local_path;
2005-06-17, by wenzelm
removed obsolete theory_of_sign, theory_of_thm;
2005-06-17, by wenzelm
PolyML.Compiler.printInAlphabeticalOrder := false;
2005-06-17, by wenzelm
Context.DATA_FAIL;
2005-06-17, by wenzelm
Context.PureN;
2005-06-17, by wenzelm
RuleCases.tactic;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
(RAW_)METHOD_CASES: RuleCases.tactic;
2005-06-17, by wenzelm
Theory.add_typedecls;
2005-06-17, by wenzelm
added map', fold;
2005-06-17, by wenzelm
Table.fold;
2005-06-17, by wenzelm
Symtab.fold;
2005-06-17, by wenzelm
type theory, theory_ref, exception THEORY and related operations imported from Context;
2005-06-17, by wenzelm
obsolete type sg is now an alias for Context.theory;
2005-06-17, by wenzelm
added theorem_space;
2005-06-17, by wenzelm
Context.theory_name;
2005-06-17, by wenzelm
added serial numbers;
2005-06-17, by wenzelm
removed obsolete pretty printers for Theory.theory, Sign.sg;
2005-06-17, by wenzelm
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
2005-06-17, by wenzelm
added type theory: generic theory contexts with unique identity,
2005-06-17, by wenzelm
removed Pure/theory_data.ML;
2005-06-17, by wenzelm
added Id;
2005-06-17, by wenzelm
Theory.merge;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
Context.theory_name;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
replaced obsolete theory_of_sign by theory_of_thm;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
refer to HOL4_PROOFS setting;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
accomodate identification of type Sign.sg and theory;
2005-06-17, by wenzelm
accomodate change of TheoryDataFun;
2005-06-17, by wenzelm
renamed sg_ref to thy_ref;
2005-06-17, by wenzelm
obsolete;
2005-06-17, by wenzelm
obsolete (see context.ML);
2005-06-17, by wenzelm
(removed experimental file)
2005-06-17, by haftmann
updated;
2005-06-17, by wenzelm
Multiple subgoals working.
2005-06-17, by quigley
migrated theory headers to new format
2005-06-17, by haftmann
grammar fix
2005-06-17, by paulson
removed redundant "open" declarations
2005-06-17, by paulson
tuned;
2005-06-16, by wenzelm
a few new integer lemmas
2005-06-16, by paulson
*** empty log message ***
2005-06-16, by nipkow
isa-migrate ++
2005-06-16, by haftmann
*** empty log message ***
2005-06-16, by nipkow
*** empty log message ***
2005-06-16, by nipkow
isa-migrate ++
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
added macos emacs hints
2005-06-16, by haftmann
isa-migrate ++
2005-06-16, by haftmann
Domain package uses ContProc for beta reduction
2005-06-15, by huffman
allow theorem attributes on fixpat declarations
2005-06-15, by huffman
fixrec package now handles mutually-recursive definitions
2005-06-15, by huffman
(undone experimental changes)
2005-06-15, by haftmann
subclassing done
2005-06-15, by haftmann
int -> IntInf.int
2005-06-15, by chaieb
added lemmas
2005-06-15, by nipkow
*** empty log message ***
2005-06-15, by nipkow
documented DUMMY
2005-06-15, by nipkow
in domain declarations, selector names are now optional
2005-06-14, by huffman
use POLY instead of DISCGARB;
2005-06-14, by wenzelm
discontinued polyml-3.x;
2005-06-14, by wenzelm
export cases_tac, induct_tac;
2005-06-14, by wenzelm
added type tactic;
2005-06-14, by wenzelm
int --> IntInt.int
2005-06-14, by chaieb
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
2005-06-14, by huffman
cleaned up and reorganized
2005-06-14, by huffman
moved continuity simproc to a separate file
2005-06-14, by huffman
up_eq and up_less in default simpset now
2005-06-14, by huffman
internalize axiom names in Defs.define; compress types via Term.compress_type
2005-06-13, by obua
downgraded to pdf v 1.4
2005-06-13, by paulson
experimental
2005-06-13, by haftmann
just non_functional experimantal code, by now
2005-06-13, by haftmann
changed -1 back to 0
2005-06-13, by nipkow
more timing information
2005-06-13, by schirmer
simp_depth now starts at -1 to make it start at 0 ;-)
2005-06-12, by nipkow
added ML-Systems/polyml-posix.ML;
2005-06-11, by wenzelm
pass ml_platform;
2005-06-11, by wenzelm
Posix patches (from polyml.ML);
2005-06-11, by wenzelm
some cygwin support;
2005-06-11, by wenzelm
* Pure/sign/theory: discontinued named name spaces;
2005-06-11, by wenzelm
renamed hide_space to hide_names;
2005-06-11, by wenzelm
renamed IsarThy.hide_space to IsarThy.hide_names;
2005-06-11, by wenzelm
name space of classes and types maintained in tsig;
2005-06-11, by wenzelm
renamed hide_classes/types/consts to hide_XXX_i;
2005-06-11, by wenzelm
discontinued named name spaces (classK, typeK, constK);
2005-06-11, by wenzelm
accomodate changed #classes;
2005-06-11, by wenzelm
accomodate changed #classes;
2005-06-11, by wenzelm
Theory.hide_consts renamed to Theory.hide_consts_i;
2005-06-11, by wenzelm
refer to name spaces values instead of names;
2005-06-11, by wenzelm
renamed Sign.intern_tycon to Sign.intern_type;
2005-06-11, by wenzelm
fixed spelling;
2005-06-11, by wenzelm
further optimizations of cycle test
2005-06-11, by obua
tuned
2005-06-10, by nipkow
tuning
2005-06-10, by nipkow
IntInf change
2005-06-10, by nipkow
All subgoals sent to the watcher at once now.
2005-06-10, by quigley
added Isar_examples/Drinker.thy;
2005-06-09, by wenzelm
full Display.pprint_theory for ML toplevel facilitates debugging;
2005-06-09, by wenzelm