Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-15, by huffman
add header
2005-09-15, by huffman
The SMLNJ Problem fixed...
2005-09-15, by chaieb
getting it work for SMLNJ
2005-09-15, by chaieb
* Improved efficiency of the Simplifier etc.;
2005-09-15, by wenzelm
incorporated into NEWS;
2005-09-15, by wenzelm
incorporated HOL/Hyperreal/CHANGES;
2005-09-15, by wenzelm
massive tidy-up and simplification
2005-09-15, by paulson
moving Commutative_Ring to the correct theory
2005-09-15, by paulson
comment
2005-09-15, by paulson
poly -doDisplay;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed type;
2005-09-15, by wenzelm
fixed ML;
2005-09-15, by wenzelm
The Hebrew Alef-Bet -- Unicode example;
2005-09-15, by wenzelm
added Hebrew.thy;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed document;
2005-09-15, by wenzelm
added HOL/ex/Hebrew.thy;
2005-09-15, by wenzelm
obsolete;
2005-09-15, by wenzelm
command 'thms_containing' has been discontinued in favour of 'find_theorems';
2005-09-15, by wenzelm
Revert previous attribute name change, problem can be avoided in JAXB.
2005-09-15, by aspinall
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
2005-09-15, by wenzelm
extend: NameSpace.default_naming;
2005-09-15, by wenzelm
the experimental tagging system, and the usual tidying
2005-09-15, by paulson
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
2005-09-15, by aspinall
AList, the_*
2005-09-15, by haftmann
fixed type annotation
2005-09-15, by haftmann
added gen_list to Pretty module
2005-09-15, by haftmann
@{term [source] ...} in subsections probably more robust;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
hide: added option '(open)';
2005-09-14, by wenzelm
imports Commutative_Ring instead of Main, since the latter hides our names;
2005-09-14, by wenzelm
hide the rather generic names used in theory Commutative_Ring;
2005-09-14, by wenzelm
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
2005-09-14, by wenzelm
... prem19
2005-09-14, by schirmer
added prem10 - prem19
2005-09-14, by schirmer
removed syntax fun_map_comp;
2005-09-14, by schirmer
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
2005-09-14, by chaieb
Method comm_ring for proving equalities in commutative rings.
2005-09-14, by wenzelm
tuned headers etc.;
2005-09-14, by wenzelm
fixed some ML names;
2005-09-14, by wenzelm
imports Commutative_Ring;
2005-09-14, by wenzelm
HOL: method comm_ring;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
no longer prefer xemacs, which fails more often than GNU emacs;
2005-09-14, by wenzelm
Bernhard Haeupler: comm_ring;
2005-09-14, by wenzelm
tactic and the rest eliminated, just the theory....
2005-09-14, by chaieb
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
(allocating new branch)
2005-08-28, by haftmann
added superclasses, class_le_path
2005-08-28, by haftmann
added alist.ML
2005-08-28, by haftmann
added 'these', removed assoc2
2005-08-28, by haftmann
added alist module
2005-08-28, by haftmann
Fixed bug.
2005-08-26, by berghofe
DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-26, by quigley
Lemmas on dvd, power and finite summation added or strengthened.
2005-08-26, by ballarin
replaced '?' by '??'
2005-08-26, by haftmann
Adapted to new code generator syntax.
2005-08-25, by berghofe
Put quotation marks around some occurrences of "file", since it is now
2005-08-25, by berghofe
Adapted to new code generator syntax.
2005-08-25, by berghofe
Implemented incremental code generation.
2005-08-25, by berghofe
fixed typo
2005-08-25, by haftmann
add_locale_context(_i) now exporting elements (still some refinements to be done)
2005-08-25, by haftmann
added ? combinator for conditional transformations
2005-08-25, by haftmann
added 'default' function
2005-08-25, by haftmann
Printing of interpretations: option to show witness theorems;
2005-08-24, by ballarin
Interpretation in locales: extended back end;
2005-08-24, by ballarin
replaced ? by ??
2005-08-23, by haftmann
fixed deps;
2005-08-19, by wenzelm
tuned arrangement of generated stuff;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
tuned generated stuff;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
obsolete;
2005-08-19, by wenzelm
tuned;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
*** empty log message ***
2005-08-19, by nipkow
updated;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
-H deleted
2005-08-19, by nipkow
ML_idf -> ML
2005-08-19, by nipkow
nicer list of axioms used
2005-08-18, by paulson
no need for TPTP2X unless SPASS is used
2005-08-18, by paulson
optimization to incr_indexes?
2005-08-18, by paulson
tuned;
2005-08-18, by wenzelm
fixed command prompt (was broken due to P.tags);
2005-08-18, by wenzelm
* The ML antiquotation prints type-checked ML expressions verbatim.
2005-08-18, by wenzelm
replace freeze by 'setmp show_question_marks false';
2005-08-18, by wenzelm
proof_to_theory_context: interaction flag;
2005-08-18, by wenzelm
accomodate interface Proof vs. Method;
2005-08-18, by wenzelm
added NO_CASES;
2005-08-18, by wenzelm
moved after method.ML;
2005-08-18, by wenzelm
prepare attributes here;
2005-08-18, by wenzelm
moved before proof.ML;
2005-08-18, by wenzelm
added add_locale_context(_i), which returns the body context for presentation;
2005-08-18, by wenzelm
moved translation functions to Pure/sign.ML;
2005-08-18, by wenzelm
various Toplevel.theory_context commands: proper presentation in context;
2005-08-18, by wenzelm
use theory instead of obsolete Sign.sg;
2005-08-18, by wenzelm
added map_specs/facts operators (from locale.ML);
2005-08-18, by wenzelm
removed obsolete Theory.sign_of;
2005-08-18, by wenzelm
load method.ML before proof.ML;
2005-08-18, by wenzelm
added interfaces for compile translation functions (from Isar/isar_thy.ML);
2005-08-18, by wenzelm
added tap;
2005-08-18, by wenzelm
updated;
2005-08-18, by wenzelm
usedir: tuned option -V;
2005-08-18, by wenzelm
usedir: removed option -H;
2005-08-18, by wenzelm
* Proper output of proof terms within a proof context;
2005-08-18, by wenzelm
Improved generation of witnesses in interpretation.
2005-08-17, by ballarin
Interpretation in locales.
2005-08-17, by ballarin
Use interpretation in locales.
2005-08-17, by ballarin
new examples
2005-08-17, by paulson
*** empty log message ***
2005-08-17, by nipkow
new command to invoke ATPs
2005-08-17, by paulson
small mods to code lemmas
2005-08-17, by nipkow
made SML/XL happy;
2005-08-17, by wenzelm
list_all_conv -> iff
2005-08-17, by nipkow
name fix
2005-08-16, by nipkow
added quite a few functions for code generation
2005-08-16, by nipkow
more simprules now have names
2005-08-16, by paulson
classical rules must have names for ATP integration
2005-08-16, by paulson
added listT
2005-08-16, by nipkow
support for document versions;
2005-08-16, by wenzelm
eliminated datatype token;
2005-08-16, by wenzelm
begin_index: list of docs;
2005-08-16, by wenzelm
added eq_syntax;
2005-08-16, by wenzelm
export proof_syntax, proof_of;
2005-08-16, by wenzelm
added String.isSuffix;
2005-08-16, by wenzelm
state: body context;
2005-08-16, by wenzelm
P.tags;
2005-08-16, by wenzelm
use_dir: removed hidden, added doc_versions;
2005-08-16, by wenzelm
back: removed ill-defined '!' option;
2005-08-16, by wenzelm
added transfer;
2005-08-16, by wenzelm
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
2005-08-16, by wenzelm
added tags parser;
2005-08-16, by wenzelm
clarify is_newline vs. is_blank;
2005-08-16, by wenzelm
default tags for theory/proof/ML commands;
2005-08-16, by wenzelm
reimplemented theory presentation, with support for tagged command regions;
2005-08-16, by wenzelm
back: removed ill-defined '!' option;
2005-08-16, by wenzelm
replaced sign by thy;
2005-08-16, by wenzelm
added liberal_name;
2005-08-16, by wenzelm
tuned Symbol.spaces;
2005-08-16, by wenzelm
tuned Buffer.add;
2005-08-16, by wenzelm
tuned unsuffix/unprefix;
2005-08-16, by wenzelm
type proof: theory_ref instead of theory (make proof contexts independent entities);
2005-08-16, by wenzelm
Isar command keyword classification (from Isar/outer_syntax.ML);
2005-08-16, by wenzelm
added Isar/outer_keyword.ML;
2005-08-16, by wenzelm
OuterKeyword;
2005-08-16, by wenzelm
updated;
2005-08-16, by wenzelm
removed -H false;
2005-08-16, by wenzelm
isatool usedir: option -V and -f;
2005-08-16, by wenzelm
tuned antiquotations;
2005-08-16, by wenzelm
\isabellestyleit: proper \isacharbackslash;
2005-08-16, by wenzelm
proper ML_DBASE for .../bin/poly;
2005-08-16, by wenzelm
added option -V VERSION;
2005-08-16, by wenzelm
added option -n NAME and -t TAGS;
2005-08-16, by wenzelm
-V outline=/proof,/ML;
2005-08-16, by wenzelm
* Command tags control specific markup of certain regions of text (replaces usedir -H);
2005-08-16, by wenzelm
simp_depth warning now mod 20, not mod 10 (too often)
2005-08-16, by nipkow
lucas - added pretty printing function and cleaned up signature a little.
2005-08-15, by dixon
lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.
2005-08-15, by dixon
New command: interpretation in locales.
2005-08-10, by ballarin
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
2005-08-09, by nipkow
exported after_qed for arity proofs
2005-08-09, by haftmann
added finite(option) to Recdef.thy
2005-08-09, by nipkow
added selectors 'classes_of' and 'classes_arities_of'
2005-08-09, by haftmann
exported dest_def
2005-08-09, by haftmann
added 'the_const_constraint'
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
After_qed takes result argument.
2005-08-08, by ballarin
Release of interpretation in locale.
2005-08-08, by ballarin
fixed typo in ratadd
2005-08-08, by nipkow
added hint for position of aqu options in connection with styles
2005-08-08, by haftmann
clarified ML_idf
2005-08-08, by haftmann
moved some rat functions to library.ML
2005-08-07, by nipkow
added more rat functions
2005-08-07, by nipkow
Tuned comment.
2005-08-06, by berghofe
new lemma
2005-08-06, by nipkow
Added ENTCS 2000 paper by Aleksey Nogin.
2005-08-05, by berghofe
New case study: pigeonhole principle.
2005-08-05, by berghofe
Added Extraction/Pigeonhole.
2005-08-05, by berghofe
added Brian Hufmann's finite instances
2005-08-05, by nipkow
Fixed bug in code generator for let and split leading to ill-formed code.
2005-08-03, by berghofe
Adapted to new argument format of MinProof constructor.
2005-08-03, by berghofe
Adapted to new interface og thms_of_proof / axms_of_proof.
2005-08-03, by berghofe
Adapted to new interface of thms_of_proof.
2005-08-03, by berghofe
- Tuned handling of oracles
2005-08-03, by berghofe
mentioned change to exp_ge_add_one_self, new transitivity rules
2005-08-03, by avigad
changes from renaming of exp_ge_add_one_self
2005-08-03, by avigad
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
2005-08-03, by avigad
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
2005-08-03, by avigad
added extra transitivity rules
2005-08-03, by avigad
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
2005-08-03, by avigad
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
2005-08-03, by avigad
import FixedPoint instead of Gfp
2005-08-03, by avigad
removed Gfp
2005-08-03, by avigad
removed Lfp
2005-08-03, by avigad
combined Lfp and Gfp to FixedPoint
2005-08-03, by avigad
tuned ML_OPTIONS;
2005-08-02, by wenzelm
export clear_ss;
2005-08-02, by wenzelm
added unfold_tac (Simplifier.inherit_bounds);
2005-08-02, by wenzelm
simprocs: Simplifier.inherit_bounds;
2005-08-02, by wenzelm
tuned;
2005-08-02, by wenzelm
First version of interpretation in locales. Not yet fully functional.
2005-08-02, by ballarin
Turned simp_implies into binary operator.
2005-08-02, by ballarin
Added filter lemma
2005-08-02, by nipkow
* Pure/Simplifier: improved handling of bound variables;
2005-08-01, by wenzelm
determine Poly/ML runtime system version
2005-08-01, by wenzelm
obsolete;
2005-08-01, by wenzelm
determine Poly/ML's idea of current hardware and operating system type;
2005-08-01, by wenzelm
tuned;
2005-08-01, by wenzelm
Thm.full_prop_of;
2005-08-01, by wenzelm
Compress.term;
2005-08-01, by wenzelm
removed atless (use term_ord instead);
2005-08-01, by wenzelm
export MataSimplifier.inherit_bounds;
2005-08-01, by wenzelm
Compress.typ;
2005-08-01, by wenzelm
Compress.init_data;
2005-08-01, by wenzelm
nameless Term.bound;
2005-08-01, by wenzelm
improved bounds: nameless Term.bound, recover names for output;
2005-08-01, by wenzelm
tuned dict_ord;
2005-08-01, by wenzelm
replaced atless by term_ord;
2005-08-01, by wenzelm
chain_history: turned into runtime flag;
2005-08-01, by wenzelm
compression of terms and types by sharing common subtrees;
2005-08-01, by wenzelm
added compress.ML;
2005-08-01, by wenzelm
Term.is_bound;
2005-08-01, by wenzelm
tuned signature;
2005-08-01, by wenzelm
no eq_commute;
2005-08-01, by wenzelm
Defs.monomorphic;
2005-08-01, by wenzelm
Sign.read_term;
2005-08-01, by wenzelm
more zcong_sym;
2005-08-01, by wenzelm
simprocs: Simplifier.inherit_bounds;
2005-08-01, by wenzelm
no eq_sym_conv;
2005-08-01, by wenzelm
removed read_cterm;
2005-08-01, by wenzelm
tuned msg;
2005-08-01, by wenzelm
PolyML.Compiler.printInAlphabeticalOrder := false;
2005-08-01, by wenzelm
polyml: use polyml-platform/version from Isabelle distribution;
2005-08-01, by wenzelm
obsolete;
2005-08-01, by wenzelm
1. changed configuration variables for linear programming (Cplex_tools):
2005-08-01, by obua
added map_filter lemmas
2005-08-01, by nipkow
Ordering is now: first by number of assumptions, second by the substitution size.
2005-08-01, by kleing
addedd ID line
2005-07-30, by nipkow
mentioned Ln in NEWS
2005-07-29, by avigad
fixed minor typo in comments
2005-07-29, by avigad
changed import to Ln
2005-07-29, by avigad
added a new theory; properties of ln
2005-07-29, by avigad
P.opt_locale_target;
2005-07-29, by wenzelm
nameless theorems: better names, flag to omit them
2005-07-29, by paulson
invents theorem names; also patches write_out_clasimp
2005-07-28, by paulson
dead code
2005-07-28, by paulson
new function trim_ends
2005-07-28, by paulson
uniform treatment of variable prefixes
2005-07-28, by paulson
corrected some typos
2005-07-28, by haftmann
new droplet
2005-07-28, by paulson
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
2005-07-28, by quigley
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip