Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-1024
+1024
+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.
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
2005-07-14, by dixon
* Improved 'oracle' command -- type-safe;
2005-07-14, by wenzelm
no open Logic;
2005-07-14, by wenzelm
removed itlist, rev_itlist -- use fold_rev, fold instead;
2005-07-14, by wenzelm
replaced itlist by fold_rev;
2005-07-14, by wenzelm
replaced itlist by fold_rev;
2005-07-14, by wenzelm
use sys_error instead of exception Internal;
2005-07-14, by wenzelm
sys_error;
2005-07-14, by wenzelm
type-safe 'oracle' command;
2005-07-14, by wenzelm
added dest_table;
2005-07-14, by wenzelm
invoke_oracle: do not keep theory value, but theory_ref;
2005-07-14, by wenzelm
occs no longer infix (structure not open);
2005-07-14, by wenzelm
NameSpace.dest_table avoids duplicated extern;
2005-07-14, by wenzelm
with_path;
2005-07-14, by wenzelm
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
2005-07-14, by wenzelm
tuned;
2005-07-14, by wenzelm
use all files in HOLCF.thy;
2005-07-14, by wenzelm
replaced Utils.itlist by fold_rev;
2005-07-14, by wenzelm
proper structure;
2005-07-14, by wenzelm
use existing Inttab;
2005-07-14, by wenzelm
improved oracle setup;
2005-07-14, by wenzelm
improved oracle setup;
2005-07-14, by wenzelm
removed not_const -- use Not instead;
2005-07-14, by wenzelm
HOL.Not;
2005-07-14, by wenzelm
HOL.Not;
2005-07-14, by wenzelm
new type-safe interface;
2005-07-14, by wenzelm
removed FOL/ex/IffOracle.ML;
2005-07-14, by wenzelm
obsolete;
2005-07-14, by wenzelm
improved 'oracle' command;
2005-07-14, by wenzelm
tuned;
2005-07-14, by wenzelm
accomodate change of real_of_XXX;
2005-07-14, by wenzelm
- fixed bug concerning the renaming of axiom names
2005-07-14, by obua
added ` combinator
2005-07-14, by haftmann
(fix for smlnj)
2005-07-14, by haftmann
simplified proof of cont_Iwhen3
2005-07-14, by huffman
avoiding even more garbage
2005-07-13, by schirmer
Update PGIP packet handling, fixing unique session identifier.
2005-07-13, by aspinall
fixed typos in theorem names
2005-07-13, by avigad
Additions to the Real (and Hyperreal) libraries:
2005-07-13, by avigad
tidied
2005-07-13, by paulson
Add ISABELLE_PID for proof_general.ML
2005-07-13, by aspinall
tuned msg;
2005-07-13, by wenzelm
added print_state_hook;
2005-07-13, by wenzelm
export previous;
2005-07-13, by wenzelm
removed ad-hoc atp_hook, cal_atp;
2005-07-13, by wenzelm
Toplevel.actual_proof;
2005-07-13, by wenzelm
avoid excessive exceptions;
2005-07-13, by wenzelm
Graph: fast_string_ord;
2005-07-13, by wenzelm
export eq_brl;
2005-07-13, by wenzelm
added subtract;
2005-07-13, by wenzelm
export eq_rrule;
2005-07-13, by wenzelm
removed obsolete delta stuff;
2005-07-13, by wenzelm
open ReconPrelim Recon_Transfer;
2005-07-13, by wenzelm
open ReconPrelim ReconTranslateProof;
2005-07-13, by wenzelm
tuned;
2005-07-13, by wenzelm
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
2005-07-13, by wenzelm
tuned concat_with_and;
2005-07-13, by wenzelm
improved Net interface;
2005-07-13, by wenzelm
* Isar session: The initial use of ROOT.ML is now always timed;
2005-07-13, by wenzelm
Add acceptedpgipelems message
2005-07-13, by aspinall
auto update
2005-07-13, by paulson
generlization of some "nat" theorems
2005-07-13, by paulson
relevance filtering is now optional
2005-07-13, by paulson
tidied
2005-07-13, by paulson
fixed comment-out;
2005-07-13, by wenzelm
fix
2005-07-13, by obua
Add management for current working directory
2005-07-13, by aspinall
(fix for an accidental commit)
2005-07-13, by haftmann
Note about theorem dependencies including themselves.
2005-07-13, by aspinall
Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
2005-07-13, by aspinall
(intermediate commit)
2005-07-13, by haftmann
(corrected wrong commit)
2005-07-13, by haftmann
(intermediate commit)
2005-07-13, by haftmann
- added cplex package to HOL/Matrix
2005-07-13, by obua
avoid some garbage
2005-07-12, by schirmer
- use TableFun instead of homebrew binary tree in am_interpreter.ML
2005-07-12, by obua
- introduce Pure/Tools directory
2005-07-12, by obua
fold_map -> fold_yield, added transformator combinators, added selector combinator
2005-07-12, by haftmann
changed orientation of bind_assoc rule
2005-07-12, by huffman
use qualified names for all constants
2005-07-12, by huffman
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
2005-07-12, by huffman
generalized types of monadic operators to class cpo; added match function for UU
2005-07-12, by huffman
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
2005-07-12, by avigad
experimental code to reduce the amount of type information in blast
2005-07-12, by paulson
tweaked
2005-07-12, by paulson
Added \<module> symbol.
2005-07-12, by berghofe
Added "attach" keyword for code generator setup.
2005-07-12, by berghofe
Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-12, by berghofe
Implemented mechanism for attaching auxiliary code to consts_code and
2005-07-12, by berghofe
small text mod
2005-07-11, by nipkow
Fixed some problems with the signal handler.
2005-07-11, by quigley
Improved implementation of Defs.is_overloaded.
2005-07-11, by obua
Some changes to allow mutually recursive, overloaded functions with same name.
2005-07-08, by berghofe
added Davenport reference
2005-07-08, by nipkow
moved Davenport citation to Main, removed author list
2005-07-08, by nipkow
moved gcd to new GCD.thy
2005-07-08, by nipkow
proof needed updating because of arith
2005-07-08, by nipkow
changed imports due to new GCD.thy
2005-07-08, by nipkow
Used to be in Library/Primes
2005-07-08, by nipkow
fix typo
2005-07-08, by huffman
replaced old continuity rules with new lemma cont2cont_lift_case
2005-07-08, by huffman
simplified proof of ifte_thms, removed ifte_simp
2005-07-08, by huffman
renamed upE1 to upE; added simp rule cont2cont_flift1
2005-07-08, by huffman
renamed upE1 to upE
2005-07-08, by huffman
define 'a u with datatype package;
2005-07-08, by huffman
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
2005-07-08, by huffman
add lemma eq_sprod
2005-07-08, by huffman
add lemma eq_cprod
2005-07-08, by huffman
removed obsolete continuity theorems
2005-07-07, by huffman
define lift type using pcpodef; cleaned up
2005-07-07, by huffman
cleaned up
2005-07-07, by huffman
fixes to work with UU_reorient_simproc
2005-07-07, by huffman
fixes to work with UU_reorient_simproc
2005-07-07, by huffman
fixes to work with UU_reorient_simproc
2005-07-07, by huffman
1) all theorems in Orderings can now be given as a parameter
2005-07-07, by obua
use theorem ch2ch_cont
2005-07-07, by huffman
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-07-07, by paulson
updated comment
2005-07-07, by paulson
add UU_reorient_simproc
2005-07-07, by huffman
use theorems ch2ch_cont, cont2contlubE
2005-07-07, by huffman
add lemmas ch2ch_cont and cont2contlubE
2005-07-07, by huffman
Preparations for interpretation of locales in locales.
2005-07-07, by ballarin
takes & in premises apart now.
2005-07-07, by nipkow
linear arithmetic is more powerful now
2005-07-07, by nipkow
linear arithmetic now takes "&" in assumptions apart.
2005-07-07, by nipkow
Used to be part of Finite_Set (or was it SetInterval?)
2005-07-07, by nipkow
fixed antiquotation;
2005-07-06, by wenzelm
removed timers;
2005-07-06, by wenzelm
debug: exception_trace;
2005-07-06, by wenzelm
finish: Output.accumulated_time;
2005-07-06, by wenzelm
dest_parsers: sort result;
2005-07-06, by wenzelm
added time_accumulator and accumulated_time supercede
2005-07-06, by wenzelm
added full_prop_of: includes tpairs;
2005-07-06, by wenzelm
tuned eq_ix;
2005-07-06, by wenzelm
Context.check_thy;
2005-07-06, by wenzelm
tuned forall_elim_var(s): avoid expensive Term.add_vars;
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
Thm.full_prop_of;
2005-07-06, by wenzelm
check_thy: less invocations, less verbose;
2005-07-06, by wenzelm
* Pure: Output.time_accumulator;
2005-07-06, by wenzelm
isatool fixheaders;
2005-07-06, by wenzelm
tuned msg;
2005-07-06, by wenzelm
ThyInfo.time_use root;
2005-07-06, by wenzelm
added output_buffer;
2005-07-06, by wenzelm
added write_list, append_list;
2005-07-06, by wenzelm
tuned write: use File.write_list;
2005-07-06, by wenzelm
tuned maxidx;
2005-07-06, by wenzelm
tuned maxidx_of_typ/typs/term;
2005-07-06, by wenzelm
multiple flags: prefer later ones;
2005-07-06, by wenzelm
use Symtab.table instead of ordered lists;
2005-07-06, by wenzelm
added adhoc string_of_term from Pure/term.ML;
2005-07-06, by wenzelm
removed term_lpo (now in Pure/term.ML);
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
tuned;
2005-07-06, by wenzelm
changed file permissions;
2005-07-06, by wenzelm
changing file permissions ...
2005-07-06, by wenzelm
add keywords cpodef, pcpodef (for HOLCF)
2005-07-06, by huffman
renamed to Pcpodef.thy
2005-07-06, by huffman
use new pcpodef package
2005-07-06, by huffman
add pcpodef files
2005-07-06, by huffman
renamed from TypedefPcpo.thy;
2005-07-06, by huffman
new type definition package for HOLCF
2005-07-06, by huffman
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
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
simplified is_stale, check_stale;
2005-06-09, by wenzelm
updated;
2005-06-09, by wenzelm
axioms: NameSpace.table;
2005-06-09, by wenzelm
PureThy.all_thms_of;
2005-06-09, by wenzelm
Theory.all_axioms_of, PureThy.all_thms_of;
2005-06-09, by wenzelm
can (Thm.get_axiom_i thy) name;
2005-06-09, by wenzelm
renamed extern to extern_thm;
2005-06-09, by wenzelm
meths: NameSpace.table;
2005-06-09, by wenzelm
NameSpace.extern_table;
2005-06-09, by wenzelm
Args.local_typ_abbrev;
2005-06-09, by wenzelm
attribs: NameSpace.table;
2005-06-09, by wenzelm
renamed global/local_typ_raw to global/local_typ_abbrev;
2005-06-09, by wenzelm
added structure Inttab;
2005-06-09, by wenzelm
added type NameSpace.table with basic operations;
2005-06-09, by wenzelm
renamed cert_typ_raw to cert_typ_abbrev;
2005-06-09, by wenzelm
axioms and oracles: NameSpace.table;
2005-06-09, by wenzelm
map_typ and map_term no longer global;
2005-06-09, by wenzelm
Major cleanup:
2005-06-09, by wenzelm
thms_of no longer global;
2005-06-09, by wenzelm
NameSpace.extern_table;
2005-06-09, by wenzelm
print_theory: omit name spaces; NameSpace.extern_table;
2005-06-09, by wenzelm
got rid of bclass, xclass;
2005-06-09, by wenzelm
add_axioms_infer -- avoids use of stale theory;
2005-06-09, by wenzelm
Theory.all_axioms_of;
2005-06-09, by wenzelm
Sign.read_typ_abbrev;
2005-06-09, by wenzelm
added chmod for packages
2005-06-09, by haftmann
added CONTRIBUTORS
2005-06-09, by haftmann
a very little cleanup
2005-06-09, by haftmann
make up_eq and up_less into simp rules
2005-06-08, by huffman
Fixed "axiom" generation for mixed locales with and without predicates.
2005-06-08, by ballarin
added some notes
2005-06-08, by haftmann
added file acces rights handling
2005-06-08, by haftmann
fix usage of inverts lemma, which has fewer premises now
2005-06-08, by huffman
faster proofs of inverts and injects lemmas, with fewer strictness hypotheses
2005-06-08, by huffman
fixed renamed lemma
2005-06-08, by huffman
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
2005-06-08, by huffman
added theorems is_ub_range_shift and is_lub_range_shift
2005-06-08, by huffman
added theorems less_sprod, spair_less, spair_eq, spair_inject
2005-06-08, by huffman
renamed theorems less_ssum4a,b,c,d to more meaningful names
2005-06-08, by huffman
added theorem less_cprod
2005-06-08, by huffman
added theorem injection_less
2005-06-08, by huffman
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
2005-06-07, by obua
extended readme
2005-06-07, by haftmann
started migration framwork script
2005-06-07, by haftmann
added basics for generic migration tool
2005-06-07, by haftmann
added isatest-lint prototype
2005-06-07, by haftmann
1) Fixed bug in Defs.merge_edges_1.
2005-06-07, by obua
*** empty log message ***
2005-06-06, by nipkow
updating...
2005-06-06, by nipkow
Added the t = x "fix" - in (* ... *) :-(
2005-06-06, by nipkow
copy_dir: be permissive wrt. errors;
2005-06-06, by wenzelm
integrated MacOS X installation instructions
2005-06-06, by haftmann
(cvs removed)
2005-06-06, by haftmann
migrated scripts to new webiste
2005-06-06, by haftmann
minor refinements
2005-06-06, by haftmann
Some error messages have been eliminated as suggested by Tobias Nipkow
2005-06-06, by chaieb
junk
2005-06-06, by nipkow
update -> use
2005-06-06, by nipkow
refinements
2005-06-06, by haftmann
Added code lemma for <
2005-06-06, by berghofe
avoid polymorphic ins;
2005-06-06, by wenzelm
fixed
2005-06-06, by kleing
added sunbroy2
2005-06-06, by haftmann
renamed const_deps to defs;
2005-06-05, by wenzelm
renamed const_deps to defs;
2005-06-05, by wenzelm
added Type.freeze(_type);
2005-06-05, by wenzelm
added the_const_type;
2005-06-05, by wenzelm
Type.freeze;
2005-06-05, by wenzelm
find empty dirs up to depth 5;
2005-06-05, by wenzelm
DISCGARB_OPTIONS back in od position;
2005-06-05, by wenzelm
link bugs fixed
2005-06-05, by haftmann
link bugs fixed
2005-06-05, by haftmann
link bugs fixed
2005-06-05, by haftmann
bugfix in record_type_abbr_tr'
2005-06-05, by schirmer
added detection for GNU cp
2005-06-05, by haftmann
added detection for GNU cp
2005-06-05, by haftmann
symlink problem hopefully solved
2005-06-05, by haftmann
better symlink handling
2005-06-05, by haftmann
a more spohisticated symlink handling
2005-06-05, by haftmann
a more spohisticated symlink handling
2005-06-05, by haftmann
a more spohisticated symlink handling
2005-06-05, by haftmann
added rsync symlink option
2005-06-05, by haftmann
typo
2005-06-05, by schirmer
added authors
2005-06-05, by haftmann
replaced File.sysify_path by Path.pack;
2005-06-05, by wenzelm
tuned msg;
2005-06-05, by wenzelm
File.isatool, File.shell_path;
2005-06-05, by wenzelm
present new-style theory header, with 'imports' and 'uses';
2005-06-05, by wenzelm
removed file_info (now in Pure/General/file.ML);
2005-06-05, by wenzelm
new Isar header: reject ':', accept both 'files' and 'uses';
2005-06-05, by wenzelm
added 'uses' keyword;
2005-06-05, by wenzelm
removed copy, copy_all (superceded by File.copy, File.copy_dir);
2005-06-05, by wenzelm
no warning for non-identifiers;
2005-06-05, by wenzelm
removed sysify_path, quote_sysity_path etc.;
2005-06-05, by wenzelm
File.platform_path vs. File.shell_path;
2005-06-05, by wenzelm
File.platform_path;
2005-06-05, by wenzelm
File.shell_path;
2005-06-05, by wenzelm
added isatool version;
2005-06-05, by wenzelm
tuned/updated antiquotations;
2005-06-05, by wenzelm
updated theory header syntax;
2005-06-05, by wenzelm
DISCGARB_OPTIONS: proper treatment of specific polyml versions;
2005-06-05, by wenzelm
observe ISABELLE_IGNORE_USER_SETTINGS;
2005-06-05, by wenzelm
Lucas Dixon;
2005-06-05, by wenzelm
* ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
2005-06-05, by wenzelm
#SMLNJ_CYGWIN_RUNTIME=1
2005-06-05, by wenzelm
added README
2005-06-04, by haftmann
fixed links
2005-06-04, by haftmann
fixed links
2005-06-04, by haftmann
fixed links
2005-06-04, by haftmann
fixed NEWS link
2005-06-04, by haftmann
added library symlink
2005-06-04, by haftmann
added library symlink
2005-06-04, by haftmann
added library symlink
2005-06-04, by haftmann
adjusted navigation width
2005-06-04, by haftmann
added shellcmd style
2005-06-04, by haftmann
added shellcmd style
2005-06-04, by haftmann
added shellcmd style
2005-06-04, by haftmann
added shellcmd style
2005-06-04, by haftmann
re-added binary files
2005-06-04, by haftmann
(temporary remove, forgotten the -b flag...)
2005-06-04, by haftmann
major reorganization and cleanup;
2005-06-04, by wenzelm
added new website
2005-06-04, by haftmann
added explicit dependency on Fix theory
2005-06-04, by huffman
add keywords fixrec and fixpat for HOLCF fixrec package
2005-06-04, by huffman
fix imports
2005-06-04, by huffman
use fixrec_package.ML
2005-06-04, by huffman
import Fix is unnecessary
2005-06-04, by huffman
added fixrec_package.ML
2005-06-04, by huffman
implementation of fixrec package
2005-06-04, by huffman
shrink session graph so it fits on a page
2005-06-04, by huffman
Domain package generates match functions for new datatypes, for use with the fixrec package
2005-06-04, by huffman
add dependency on Fixrec.thy
2005-06-04, by huffman
add Fixrec.thy
2005-06-04, by huffman
New theory with lemmas for the fixrec package
2005-06-04, by huffman
changed variable name in monofun_cfun_arg
2005-06-03, by huffman
fixed renamed theorems
2005-06-03, by huffman
fixed some renamed theorems
2005-06-03, by huffman
renamed defined lemmas
2005-06-03, by huffman
renamed variable in cont2cont_app
2005-06-03, by huffman
changed to use new contlubI, etc.
2005-06-03, by huffman
cleaned up proof of cont_Ifix
2005-06-03, by huffman
replaced cont with cont_def
2005-06-03, by huffman
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
2005-06-03, by huffman
changed to use new contI; renamed strict, defined, and inject lemmas
2005-06-03, by huffman
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
2005-06-03, by huffman
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
2005-06-03, by huffman
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
2005-06-03, by huffman
changed to work with new contlubE rule
2005-06-03, by huffman
renamed FunCpo to Ffun
2005-06-03, by huffman
renamed to Ffun (full function space)
2005-06-03, by huffman
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
2005-06-03, by huffman
added theorem ch2ch_lub
2005-06-03, by huffman
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
2005-06-03, by huffman
added theorems diag_lub and ex_lub
2005-06-03, by huffman
fixed a typo in the gfp interpreter
2005-06-03, by webertj
no longer emits literals for type class HOL.type; also minor tidying
2005-06-03, by paulson
Integrates cycle detection in definitions with finalconsts
2005-06-03, by obua
tuned msgs;
2005-06-02, by wenzelm
html_syms table;
2005-06-02, by wenzelm
tuned;
2005-06-02, by wenzelm
Output.no_warnings;
2005-06-02, by wenzelm
tuned comment;
2005-06-02, by wenzelm
exists: made non-strict;
2005-06-02, by wenzelm
added no_warnings;
2005-06-02, by wenzelm
Sign.restore_naming;
2005-06-02, by wenzelm
replaced set_naming by restore_naming;
2005-06-02, by wenzelm
replaced foldl_string by fold_string;
2005-06-02, by wenzelm
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
2005-06-02, by wenzelm
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
2005-06-02, by wenzelm
Added time lime (60 secs) to Spass calls.
2005-06-02, by quigley
renamed "constrains" to "safety" to avoid keyword clash
2005-06-02, by paulson
renamed "constrains" to "safety" to avoid keyword clash
2005-06-02, by paulson
swap declaration of thm/axm names to accomodate change in name space
2005-06-02, by wenzelm
tuned;
2005-06-02, by wenzelm
Theory.restore_naming;
2005-06-02, by wenzelm
header;
2005-06-02, by wenzelm
reduced timeout, send logs also when test taking too long
2005-06-02, by kleing
Preliminary version of defs.ML that does not check final consts.
2005-06-01, by obua
*** empty log message ***
2005-06-01, by nipkow
tuned
2005-06-01, by nipkow
ordering for the ordinals
2005-06-01, by paulson
clausification bug fix
2005-06-01, by paulson
small tweaks; also now write_out_clasimp takes the current theory as argument
2005-06-01, by paulson
remove CVS id from *.sty latex styles
2005-06-01, by haftmann
remove CVS id from *.sty latex styles
2005-06-01, by haftmann
Locales: new element constrains, parameter renaming with syntax,
2005-06-01, by ballarin
Locales: new element constrains, parameter renaming with syntax,
2005-06-01, by ballarin
renamed premise* to prem
2005-06-01, by haftmann
some refinements
2005-06-01, by haftmann
concl antiqutations
2005-06-01, by haftmann
*** empty log message ***
2005-06-01, by nipkow
improved *.sty handling
2005-06-01, by haftmann
improved *.sty handling
2005-06-01, by haftmann
improved *.sty handling
2005-06-01, by haftmann
added premise<i>
2005-06-01, by nipkow
added dependency
2005-06-01, by nipkow
Removed final_consts from theory data. Now const_deps deals with final
2005-05-31, by obua
minor tidying and sml/nj compatibility
2005-05-31, by paulson
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
2005-05-31, by quigley
fixed sectioning
2005-05-31, by nipkow
\nexists
2005-05-31, by nipkow
\nexists und premsise1 .. 9
2005-05-31, by nipkow
no_tac;
2005-05-31, by wenzelm
ML Pure: name spaces have been refined;
2005-05-31, by wenzelm
moved is_ident to General/symbol.ML;
2005-05-31, by wenzelm
Theory.restore_naming;
2005-05-31, by wenzelm
make: T option -- actually remove undefined cases;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
method_cases: RuleCases.T option;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
improved naming of complex theorems in presentation;
2005-05-31, by wenzelm
added short_names, unique_names options;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
added symbol scanner;
2005-05-31, by wenzelm
remove(_multi): generalized type;
2005-05-31, by wenzelm
added is_ident (from Syntax/lexicon.ML);
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned arrangement of structures;
2005-05-31, by wenzelm
added eq_thms;
2005-05-31, by wenzelm
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned msg;
2005-05-31, by wenzelm
added nth_prem;
2005-05-31, by wenzelm
export filter;
2005-05-31, by wenzelm
Sign.declare_name replaces NameSpace.extend;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
fixed outer syntax: allow type_args with parentheses;
2005-05-31, by wenzelm
proper use of Sign.full_name;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
Theory.restore_naming;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
antiquotations: added options short_names, unique_names;
2005-05-31, by wenzelm
improved naming of complex theorems in presentation;
2005-05-31, by wenzelm
removed;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-30, by wenzelm
Infinite chains in definitions are now detected, too.
2005-05-30, by obua
typo
2005-05-30, by kleing
updated para on searching
2005-05-30, by kleing
added \nexists
2005-05-30, by nipkow
Removes an inconsistent definition from Library.thy ,
2005-05-29, by obua
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
2005-05-29, by obua
make COPYRIGHT file available for web page
2005-05-29, by kleing
path /home/stud doesn't exist on macbroy33 (only /usr/stud)
2005-05-28, by kleing
SML/NJ compatibility.
2005-05-27, by ballarin
Typo.
2005-05-27, by ballarin
Deleted old code.
2005-05-27, by ballarin
Locale expressions: rename with optional mixfix syntax.
2005-05-27, by ballarin
Add back rudely removed and popular -X option.
2005-05-27, by aspinall
Now uses File.write and File.append
2005-05-27, by paulson
removed obsolete theorems
2005-05-27, by huffman
use TypedefPcpo for all class instances
2005-05-27, by huffman
log more failure types
2005-05-27, by kleing
added lemmas monofun_lub_fun and cont_lub_fun
2005-05-27, by huffman
put global isatest settings in one file, sourced by the other scripts
2005-05-27, by kleing
Use TypedefPcpo theorem for po instance
2005-05-27, by huffman
use thelub_const lemma
2005-05-27, by huffman
added lemma thelub_const
2005-05-27, by huffman
further tweaks to the SPASS setup
2005-05-26, by paulson
goodby to modUnix
2005-05-26, by paulson
trying to set up portable calling sequences for SPASS and tptp2X
2005-05-26, by paulson
cleaned up select_match
2005-05-26, by kleing
Narrower version of the Proof General's head; removal of the alternative icon and environment
2005-05-26, by paulson
Narrower version of the Proof General's head
2005-05-26, by paulson
rewrote continuous isomorphism section, cleaned up
2005-05-26, by huffman
cleaned up, added UU_app and less_funI, removed some obsolete stuff
2005-05-26, by huffman
added defaultsort declaration, moved cpair_less to Cprod.thy
2005-05-26, by huffman
added defaultsort declaration
2005-05-26, by huffman
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
2005-05-26, by huffman
removed dependence on Cfun.thy
2005-05-26, by huffman
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
2005-05-26, by huffman
new Brouwer ordinal example
2005-05-25, by paulson
more cleanup
2005-05-25, by kleing
tuned thm_style section
2005-05-25, by kleing
added ? explanations
2005-05-25, by nipkow
renamed search criterion 'rewrite' to 'simp'
2005-05-25, by kleing
SML/NJ compatibility
2005-05-25, by paulson
new environments for Proof General notes
2005-05-25, by paulson
removed obsolete findI, findE, findEs
2005-05-25, by kleing
removed LICENCE note -- everything is subject to Isabelle licence as
2005-05-25, by wenzelm
*** empty log message ***
2005-05-25, by nipkow
grammar
2005-05-25, by nipkow
shorted proof that lift is chfin
2005-05-25, by huffman
Removed shell variables. Now uses isatool getenv -b SPASS_HOME.
2005-05-25, by quigley
Generic version of spassshell. Add SPASS_HOME to .bashrc so that shell script can find it.
2005-05-24, by quigley
ML_idf antiquotation
2005-05-24, by haftmann
oracle example converted to Isar
2005-05-24, by paulson
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24, by paulson
A new structure and reduced indentation
2005-05-24, by paulson
Simplified version of strict sum theory, using TypedefPcpo
2005-05-24, by huffman
Simplified version of strict product theory, using TypedefPcpo
2005-05-24, by huffman
New theory for defining subtypes of pcpos
2005-05-24, by huffman
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
2005-05-24, by huffman
Moved admissibility definitions and lemmas to a separate theory
2005-05-24, by huffman
moved continuity simproc to Cfun.thy
2005-05-23, by huffman
moved continuity simproc to Cont.thy
2005-05-23, by huffman
moved theorem cont2cont_CF1L_rev2 to Cont.thy
2005-05-23, by huffman
tuned setsum rewrites
2005-05-23, by nipkow
* Pure/Syntax: In schematic variable names, *any* symbol following
2005-05-23, by wenzelm
interpreters for lfp/gfp added
2005-05-23, by webertj
obsolete;
2005-05-23, by wenzelm
spassshell and testout.py are used to filter the proof part out of SPASS's
2005-05-23, by quigley
tuned pretty_sg;
2005-05-23, by wenzelm
node_trans: revert to original transaction code (pre 1.54);
2005-05-23, by wenzelm
use: not a theory command!
2005-05-23, by wenzelm
converted back from 0..< to <.
2005-05-23, by nipkow
added email
2005-05-23, by haftmann
tuned trace info (depth)
2005-05-23, by nipkow
simplifier trace info; Suc-intervals
2005-05-23, by nipkow
some adaptions
2005-05-23, by haftmann
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
2005-05-23, by quigley
tuned;
2005-05-22, by wenzelm
string FindTheorems.criterion;
2005-05-22, by wenzelm
added read_criterion/pretty_criterion;
2005-05-22, by wenzelm
added show_dummy_patterns;
2005-05-22, by wenzelm
updated;
2005-05-22, by wenzelm
Retrieve theorems from proof context -- improved version of
2005-05-22, by wenzelm
added Pure/simplifier.ML, Pure/Isar/find_theorems.ML;
2005-05-22, by wenzelm
moved everything related to thms_containing to find_theorems.ML;
2005-05-22, by wenzelm
added reserved;
2005-05-22, by wenzelm
added ident_with;
2005-05-22, by wenzelm
fold ProofContext.declare_term;
2005-05-22, by wenzelm
added 'print_simpset';
2005-05-22, by wenzelm
added print_simpset;
2005-05-22, by wenzelm
added find_theorems.ML, ../simplifier.ML;
2005-05-22, by wenzelm
tuned terms_of_tpairs;
2005-05-22, by wenzelm
added string_of_thmref, selections, fact_index_of, valid_thms;
2005-05-22, by wenzelm
FindTheorems.print_theorems;
2005-05-22, by wenzelm
findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;
2005-05-22, by wenzelm
major tuning;
2005-05-22, by wenzelm
Simplifier already setup in Pure;
2005-05-22, by wenzelm
tuned antiquotations;
2005-05-22, by wenzelm
tuned thms_containing;
2005-05-22, by wenzelm
tuned;
2005-05-22, by wenzelm
moved to Pure;
2005-05-22, by wenzelm
moved here from Provers;
2005-05-22, by wenzelm
removed find_rewrites (superceded by improved thms_containing);
2005-05-22, by wenzelm
bug fixes for clause form transformation
2005-05-20, by paulson
converted some problems to Isar format
2005-05-20, by paulson
subst again
2005-05-19, by nipkow
Skolemization of simprules and classical rules
2005-05-19, by paulson
pcpo instance for type unit
2005-05-19, by huffman
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
2005-05-19, by dixon
shortened proof of adm_disj
2005-05-18, by huffman
cleaned up and shortened some proofs
2005-05-18, by huffman
lucas - fixed subst in assumptions to count redexes from left to right.
2005-05-18, by dixon
removed update_node, which is just an instance of map_node;
2005-05-18, by wenzelm
tuned;
2005-05-18, by wenzelm
updated;
2005-05-18, by wenzelm
searching for combination of criteria (intro, elim, dest, name, pattern)
2005-05-18, by kleing
made para on searching more readable
2005-05-18, by kleing
new cnf function taking Skolemization theorems as an extra argument
2005-05-18, by paulson
consolidation and simplification
2005-05-18, by paulson
documented new thms_containing ('rewrites' still missing)
2005-05-18, by kleing
documented new subst
2005-05-18, by nipkow
proper Id line;
2005-05-17, by wenzelm
updated;
2005-05-17, by wenzelm
var_or_skolem: always print question mark for vars stemming from skolems;
2005-05-17, by wenzelm
added read_variable: optional question mark on input;
2005-05-17, by wenzelm
substantial tuning -- adapted to common conventions;
2005-05-17, by wenzelm
re-init ml_prompts after loop termination;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
Syntax.read_variable;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
updated;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
removed ISAMODE settings;
2005-05-17, by wenzelm
no longer support isa-FOO interface;
2005-05-17, by wenzelm
no longer support isa-FOO interface;
2005-05-17, by wenzelm
tuned;
2005-05-17, by wenzelm
obsolete;
2005-05-17, by wenzelm
added comment
2005-05-17, by paulson
streamlined proof using new subst method
2005-05-17, by paulson
moved credit to CONTRIBUTORS;
2005-05-17, by wenzelm
moved credit to CONTRIBUTORS;
2005-05-17, by wenzelm
tuned;
2005-05-17, by wenzelm
export ISABELLE_HOME, do not normalize;
2005-05-17, by wenzelm
removed THIS_IS_ISABELLE_ADMIN;
2005-05-17, by wenzelm
removed rev_append;
2005-05-17, by wenzelm
obsolete;
2005-05-17, by wenzelm
added;
2005-05-17, by wenzelm
proper treatment of directory links;
2005-05-17, by wenzelm
use Drule.vars_of_terms
2005-05-17, by kleing
Use of IntInf.int instead of int in most numeric simprocs; avoids
2005-05-16, by paulson
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-05-16, by kleing
export parser for "-"
2005-05-16, by kleing
line wrap
2005-05-16, by kleing
Eta-expanded merge function (to make SmlNJ happy).
2005-05-15, by berghofe
added Proof.context to antiquotation
2005-05-14, by haftmann
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
2005-05-13, by dixon
-(n::nat) is now regarded as atomic
2005-05-13, by nipkow
Bugfix in syntax translation for record type.
2005-05-13, by schirmer
theorem names for caching
2005-05-12, by paulson
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
2005-05-12, by paulson
first-order now ignores "all"
2005-05-12, by paulson
fixed a few things and added Haftmann as author
2005-05-12, by nipkow
documented new subst method
2005-05-11, by paulson
corrections
2005-05-11, by haftmann
Added thms by Brian Huffmann
2005-05-11, by nipkow
new cterm primitives
2005-05-10, by paulson
oops...cannot use subst here
2005-05-10, by paulson
table centering, headline 'other platform'
2005-05-10, by kleing
unfolding of Ex1
2005-05-09, by paulson
choice_const moved to hologic.ML
2005-05-09, by paulson
from simplesubst to new subst
2005-05-09, by paulson
minor corrections
2005-05-09, by haftmann
made file links local, smoothed text over in some places
2005-05-09, by kleing
made file list nicer
2005-05-09, by kleing
moved description (dist area) out of link
2005-05-09, by kleing
made download links local, provide explicit list of files to download
2005-05-09, by kleing
shortened
2005-05-09, by kleing
MAILTO: makarius@sketis.net
2005-05-08, by wenzelm
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
2005-05-06, by dixon
added notes for mac os
2005-05-06, by haftmann
Added notes for installation on Windows
2005-05-06, by haftmann
added option 'tidy=' to makefile, for optional processing of results by HTML tidy
2005-05-06, by haftmann
replaced some outdated HTML by more modern constructs
2005-05-06, by haftmann
added new antiquotations
2005-05-06, by haftmann
Replaced all unnecessary uses of SOME with THE or LEAST
2005-05-06, by huffman
lucas - added option to select occurance to rewrite e.g. (occ 4)
2005-05-05, by dixon
lucas - made clean unify smash unifiers so that when we get flex-flex constraints subst does not barf. Also added fix_vars_upto_idx to IsaND.
2005-05-05, by dixon
lucas - added update node function.
2005-05-05, by dixon
Added eta_long attribute.
2005-05-04, by berghofe
Added eta_long_conversion.
2005-05-04, by berghofe
eta-expansion
2005-05-04, by paulson
fixed lin.arith
2005-05-04, by nipkow
neqE applies even if the type is not one which partakes in linear arithmetic.
2005-05-04, by nipkow
Fixing a problem with lin.arith.
2005-05-04, by nipkow
make mkdir usable with cygwin
2005-05-03, by haftmann
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
2005-05-03, by quigley
final implementation of antiquotations styles
2005-05-03, by haftmann
Added short description of thm_style and term_style antiquotation
2005-05-03, by haftmann
*** empty log message ***
2005-05-03, by nipkow
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
2005-05-03, by dixon
lucas - added dest_TVar and dest_TFree.
2005-05-03, by dixon
Removed nodup_vars avoiding hack
2005-05-02, by schirmer
fixed
2005-05-02, by nipkow
turned 2 lemmas into simp rules
2005-05-02, by nipkow
*** empty log message ***
2005-05-02, by nipkow
fixed setsum problem
2005-05-02, by nipkow
meta-logic connectives now forbidden
2005-05-02, by paulson
deleted redundant code
2005-05-02, by paulson
fixed reference to top-level
2005-05-02, by paulson
introduced @{const ...} antiquotation
2005-05-02, by haftmann
introduced @{const ...} antiquotation
2005-05-02, by haftmann
added to isatest-doc MAILTO
2005-05-02, by haftmann
added myself to mailing list
2005-05-02, by nipkow
superceded by IsarOverview
2005-05-02, by kleing
fixed typo
2005-04-30, by kleing
separate test run for theories in Doc/
2005-04-30, by kleing
use absolute path to find LaTeXSugar and OptionalSugar
2005-04-30, by kleing
export DISTPREFIX to devel page Makefile
2005-04-30, by isatest
fixed dependencies
2005-04-30, by kleing
don't leave stale root.pdf / root.dvi
2005-04-30, by kleing
move generated files to document/ to avoid CVS file overwrite in generated/
2005-04-30, by kleing
move generated files to document/, avoid CVS file overwrite in generated/
2005-04-30, by kleing
unused
2005-04-30, by kleing
removed obsolete exercise collection (is now in coursematerial)
2005-04-30, by kleing
updated PG preview for new thms-containing
2005-04-29, by paulson
better error reporting
2005-04-29, by paulson
put 8h time limit on test
2005-04-29, by kleing
move isadist to ~/tmp/
2005-04-29, by kleing
publish only *.html
2005-04-29, by kleing
include new thms_containing
2005-04-29, by kleing
credits
2005-04-29, by kleing
new thms_containing that searches for patterns instead of constants
2005-04-29, by kleing
new thms_containing that searches for patterns instead of constants
2005-04-29, by kleing
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
2005-04-29, by haftmann
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
2005-04-29, by haftmann
version update
2005-04-29, by kleing
include x86_64
2005-04-29, by kleing
make symlink handling compatible with whitespaces
2005-04-28, by wenzelm
sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances);
2005-04-28, by wenzelm
added plain_prop_of;
2005-04-28, by wenzelm
added smart_conjunction_tac, prove_multi, prove_multi_standard;
2005-04-28, by wenzelm
auto update
2005-04-28, by paulson
fixed treatment of higher-order simprules
2005-04-28, by paulson
*** empty log message ***
2005-04-28, by bauerg
more on rev
2005-04-28, by kleing
intersection
2005-04-28, by kleing
more about list_update
2005-04-28, by kleing
some more lemmas about multiset_of
2005-04-28, by kleing
sped up a bit
2005-04-28, by kleing
removed --version which is not a valid polyml flag and has no effect
2005-04-27, by gagern
make symlink handling compatible with whitespaces
2005-04-27, by gagern
minor tidying
2005-04-27, by paulson
removed unnecessary (?) check
2005-04-27, by paulson
tidied
2005-04-27, by paulson
partial modernising of theory headers
2005-04-27, by paulson
bug in plusinf and mininf for the oracle fixed.
2005-04-27, by chaieb
reverted last change (dependencies in HOL)
2005-04-27, by kleing
Added binder syntax for fix
2005-04-27, by huffman
removed -a option;
2005-04-26, by wenzelm
lucas - updated to reflect isand.ML update
2005-04-26, by dixon
lucas - improved comments, clarified function behaviour, added missing functions for working with meta variables.
2005-04-26, by dixon
export intro_classes_tac;
2005-04-26, by wenzelm
allow symlinks to all proper Isabelle executables;
2005-04-26, by wenzelm
eval command line: show results;
2005-04-26, by wenzelm
no longer need feeder to run normal interactive sessions;
2005-04-26, by wenzelm
tuned;
2005-04-26, by wenzelm
restored AUTO_BASH/PERL -- beware of ./configure!
2005-04-26, by wenzelm
restored AUTO_BASH/PERL -- beware of ./configure!
2005-04-26, by wenzelm
reverted accidental commit of user modification;
2005-04-26, by wenzelm
ALL_LOGICS: topological order;
2005-04-26, by wenzelm
improved handling of symlinks;
2005-04-26, by wenzelm
improved handling of symlinks;
2005-04-26, by wenzelm
eta-expanded a function
2005-04-26, by paulson
HTML standard conformity: done
2005-04-26, by webertj
test sml/nj devel only for the moment
2005-04-26, by isatest
Fixed bug in fact activation.
2005-04-26, by ballarin
*** empty log message ***
2005-04-25, by nipkow
Subsumption of locale interpretations.
2005-04-25, by ballarin
tuned comment;
2005-04-23, by wenzelm
added tokentrans_mode, standard_token_classes, standard_token_markers (from token_trans.ML);
2005-04-23, by wenzelm
SynExt.standard_token_markers
2005-04-23, by wenzelm
less
more
|
(0)
-10000
-1024
+1024
+10000
+30000
tip