isabelle: Graph

use was wrong...
2005-09-14, by chaieb
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
2005-09-14, by obua
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
2005-09-14, by chaieb
introduced AList.lookup
2005-09-14, by haftmann
correct E brackets
2005-09-14, by paulson
nice names for more infix operators
2005-09-14, by paulson
introduces AList.lookup
2005-09-14, by haftmann
removed duplicated lemmas; convert more proofs to transfer principle
2005-09-14, by huffman
add theorem chain_const
2005-09-13, by huffman
tuned;
2005-09-13, by wenzelm
global quick_and_dirty;
2005-09-13, by wenzelm
Printing of Isar proof elements etc.
2005-09-13, by wenzelm
Non-empty stacks.
2005-09-13, by wenzelm
IsarThy.begin_theory;
2005-09-13, by wenzelm
export ml_exts;
2005-09-13, by wenzelm
begin_theory: tuned interface, check uses;
2005-09-13, by wenzelm
replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-13, by wenzelm
added three_buffersN, print3;
2005-09-13, by wenzelm
load before proof.ML;
2005-09-13, by wenzelm
added simple;
2005-09-13, by wenzelm
added add_view, export_view (supercedes adhoc view arguments);
2005-09-13, by wenzelm
major cleanup of interfaces and implementation;
2005-09-13, by wenzelm
added name_facts;
2005-09-13, by wenzelm
tuned Isar proof elements;
2005-09-13, by wenzelm
added cheating, sorry_text (from skip_proofs.ML);
2005-09-13, by wenzelm
load late, after proof.ML;
2005-09-13, by wenzelm
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
2005-09-13, by wenzelm
cleanup parsers and interfaces;
2005-09-13, by wenzelm
Proof.get_thmss;
2005-09-13, by wenzelm
tuned;
2005-09-13, by wenzelm
more self-contained proof elements (material from isar_thy.ML);
2005-09-13, by wenzelm
added cases, rule_contextN;
2005-09-13, by wenzelm
load locale.ML late (after proof.ML);
2005-09-13, by wenzelm
added maps, map_list, lift, lifts;
2005-09-13, by wenzelm
added stack.ML;
2005-09-13, by wenzelm
added simple_fact;
2005-09-13, by wenzelm
Seq.maps;
2005-09-13, by wenzelm
added hide_names(_i) (from isar_thy.ML);
2005-09-13, by wenzelm
added generic_setup, add_oracle (from isar_thy.ML);
2005-09-13, by wenzelm
added exception EXCEPTION of exn * string;
2005-09-13, by wenzelm
replaced DATA_FAIL by EXCEPTION;
2005-09-13, by wenzelm
tuned Isar interfaces;
2005-09-13, by wenzelm
added General/stack.ML, Isar/proof_display.ML;
2005-09-13, by wenzelm
the_list (cf. Pure/library.ML);
2005-09-13, by wenzelm
tuned IsarThy.theorem_i;
2005-09-13, by wenzelm
fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-13, by obua
list of constants and theorems whose names have been changed or merged
2005-09-12, by huffman
add header
2005-09-12, by huffman
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12, by huffman
updated to work with latest HOL-Complex
2005-09-12, by huffman
add file Hyperreal/transfer.ML
2005-09-12, by huffman
new implementation of transfer principle
2005-09-12, by huffman
removed clutter
2005-09-12, by obua
name conflict with global itrev resolved
2005-09-12, by nipkow
dealt with name clash with List.itrev
2005-09-12, by nipkow
introduced new-style AList operations
2005-09-12, by haftmann
introduced internal function hthm2thm
2005-09-12, by obua
1) Added target HOL-Complex-Generate-HOLLight
2005-09-12, by obua
Added HOLLight support to importer.
2005-09-12, by obua
added interact flag to control mode of excursions;
2005-09-12, by wenzelm
excursion: interactive if debug;
2005-09-11, by wenzelm
updated to work with new HOL-Complex version
2005-09-09, by huffman
starfun, starset, and other functions on NS types are now polymorphic;
2005-09-09, by huffman
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09, by paulson
fixed printing of locales
2005-09-09, by ballarin
consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08, by paulson
introduces some modern-style AList operations
2005-09-08, by haftmann
added the_list, the_default
2005-09-08, by haftmann
yet more tidying of Isabelle-ATP link
2005-09-08, by paulson
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
removed TLA/Inc/Pcount.thy;
2005-09-07, by wenzelm
elimination of watcher.sig
2005-09-07, by paulson
Progress on eprover linkup, also massive tidying
2005-09-07, by paulson
axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07, by paulson
consolidation of watcher.ML and watcher.sig
2005-09-07, by paulson
generalized types more
2005-09-07, by huffman
generalized types
2005-09-07, by huffman
added theorem hypreal_inverse2
2005-09-07, by huffman
replace type hcomplex with complex star
2005-09-07, by huffman
replace type hypnat with nat star
2005-09-07, by huffman
replace type hypreal with real star
2005-09-06, by huffman
add Hyperreal dependencies
2005-09-06, by huffman
class instances for nonstandard types
2005-09-06, by huffman
transfer principle tactic
2005-09-06, by huffman
generic nonstandard type constructor
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
fix proof
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
reimplement Filter.thy with locales
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
removed some ML files in Modelcheck/;
2005-09-06, by wenzelm
updated;
2005-09-06, by wenzelm
axclass: no longer bind "cI";
2005-09-06, by wenzelm
deprecated old-style infix declarations, which mix name and syntax;
2005-09-06, by wenzelm
tuned msg;
2005-09-06, by wenzelm
AList.defined;
2005-09-06, by wenzelm
name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
proper treatment of polymorphic sets;
2005-09-06, by wenzelm
tuned comments;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
make LocalesTest last, because it sets funny flags;
2005-09-06, by wenzelm
avoid old-style infixes;
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
unnecessary parentheses removed
2005-09-06, by webertj
converted to Isar theory format;
2005-09-06, by wenzelm
introduced some new-style AList operations
2005-09-06, by haftmann
eliminated 1 call to polyEq
2005-09-06, by haftmann
tuned;
2005-09-05, by wenzelm
updated;
2005-09-05, by wenzelm
obsolete;
2005-09-05, by wenzelm
added assert, command;
2005-09-05, by wenzelm
tuned check_text;
2005-09-05, by wenzelm
chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
markup commands: optional locale specification;
2005-09-05, by wenzelm
add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
curried_lookup/update;
2005-09-05, by wenzelm
tuned;
2005-09-05, by wenzelm
Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-05, by wenzelm
removed duplicate theorems;
2005-09-05, by wenzelm
introduced binding priority 1 for linear combinators etc.
2005-09-05, by haftmann
converted to Isar theory format;
2005-09-03, by wenzelm
tuned method;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
obsolete;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
obsolete (see Cube.thy);
2005-09-03, by wenzelm
tuned msg;
2005-09-03, by wenzelm
uses ("LCF_lemmas.ML");
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
removed fix.thy, pair.thy, simpdata.ML;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
setmp print_mode []; more robust outer syntax; tuned;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
simplified oracle;
2005-09-03, by wenzelm
use Check.ML;
2005-09-03, by wenzelm
fixed ML errors;
2005-09-03, by wenzelm
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
2005-09-03, by wenzelm
deprecated non-Isar theory file format;
2005-09-03, by wenzelm
Added ECommunication.ML
2005-09-02, by quigley
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
2005-09-02, by quigley
further tidying up of Isabelle-ATP link
2005-09-02, by paulson
converted specifications to Isar theories;
2005-09-02, by wenzelm
some 'assoc' etc. refactoring
2005-09-02, by haftmann
tidying up the Isabelle/ATP interface
2005-09-02, by paulson
fixed arities and restored changes that had gone missing
2005-09-02, by paulson
deleted obsolete VampireCommunication.ML
2005-09-02, by paulson
print_locale omits facts by default
2005-09-02, by ballarin
curried_lookup/update;
2005-09-01, by wenzelm
refrain from sorting output;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
added curried_lookup/update operations -- in preparation of currying plain lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
updated;
2005-09-01, by wenzelm
renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;
2005-09-01, by wenzelm
removed obsolete 'symbols' mode;
2005-09-01, by wenzelm
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
2005-09-01, by wenzelm
improved formatting
2005-09-01, by paulson
isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
2005-09-01, by wenzelm
updated;
2005-09-01, by wenzelm
fixed ins_tokentr: AList.default;
2005-08-31, by wenzelm
comp -> compile
2005-08-31, by nipkow
Additional BigO lemmas that require the HOL-Complex logic image;
2005-08-31, by wenzelm
added copy-dump option;
2005-08-31, by wenzelm
added line break for 'uses';
2005-08-31, by wenzelm
added no_body_context;
2005-08-31, by wenzelm
use_dir: added copy-dump option;
2005-08-31, by wenzelm
present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
2005-08-31, by wenzelm
refer to theory instead of low-level tsig;
2005-08-31, by wenzelm
tuned classes_arities_of;
2005-08-31, by wenzelm
refer to theory instead of low-level tsig;
2005-08-31, by wenzelm
added Avigad-Donnelly;
2005-08-31, by wenzelm
reactivate postfix by change of syntax;
2005-08-31, by wenzelm
tuned presentation;
2005-08-31, by wenzelm
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
2005-08-31, by wenzelm
added Complex/ex/BigO_Complex.thy;
2005-08-31, by wenzelm
simp_implies: proper named infix;
2005-08-31, by wenzelm
tuned;
2005-08-31, by wenzelm
isatool usedir: added option -C;
2005-08-31, by wenzelm
added option -C: copy existing document directory;
2005-08-31, by wenzelm
* Delimiters of outer tokens now produce separate LaTeX macros;
2005-08-31, by wenzelm
introduced AList.*
2005-08-31, by haftmann
better map_entry
2005-08-31, by haftmann
fixed bug in record_type_abbr_tr'
2005-08-30, by schirmer
patterns in setsum and setprod
2005-08-30, by paulson
Updated import.
2005-08-29, by obua
updated;
2005-08-29, by wenzelm
delimiter markup for verbatim tokens;
2005-08-29, by wenzelm
clarify type tok, do not emit markup flag for suppressed tokens;
2005-08-29, by wenzelm
use AList operations;
2005-08-29, by wenzelm
cover tagged command regions;
2005-08-29, by wenzelm
tune spacing where a generated theory text is included directly;
2005-08-29, by wenzelm
updated;
2005-08-29, by wenzelm
recover original definitions of \isactrlsub etc.;
2005-08-29, by wenzelm
canonical interface for 'default'
2005-08-29, by haftmann
output \<^loc> as 'loc' span;
2005-08-28, by wenzelm
isatool latex -o sty;
2005-08-28, by wenzelm
added 'loc';
2005-08-28, by wenzelm
updated;
2005-08-28, by wenzelm
ASCII back-quote no longer sym char;
2005-08-28, by wenzelm
added \isactrlloc;
2005-08-28, by wenzelm
* ML functions legacy_bindings and use_legacy_bindings;
2005-08-28, by wenzelm
avoid symbolic identifier;
2005-08-28, by wenzelm
added (use_)legacy_bindings;
2005-08-28, by wenzelm
output_basic: handle AltString token;
2005-08-28, by wenzelm
removed obsolete type_syn;
2005-08-28, by wenzelm
unskolem local vars;
2005-08-28, by wenzelm
tuned;
2005-08-28, by wenzelm
added alt_string;
2005-08-28, by wenzelm
added AltString token (delimited by ASCII back-quotes);
2005-08-28, by wenzelm
removed unused dest operation;
2005-08-28, by wenzelm
export theorems_of;
2005-08-28, by wenzelm
tuned some proofs;
2005-08-28, by wenzelm
removed obsolete arities;
2005-08-28, by wenzelm
tuned size of included graph;
2005-08-28, by wenzelm
added \isachardoublequoteopen/close, \isacharbackquoteopen/close;
2005-08-28, by wenzelm
(branch cleanup)
2005-08-28, by haftmann