Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+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.
mksimps and mk_eq_True no longer raise THM exception.
2001-09-28, by berghofe
Added label for section on terms.
2001-09-28, by berghofe
Added documentation for proof terms.
2001-09-28, by berghofe
Added TYPE to Pure grammar.
2001-09-28, by berghofe
Added \ttlbrack and \ttrbrack.
2001-09-28, by berghofe
Added TPHOLs2000 paper about proof terms.
2001-09-28, by berghofe
updated;
2001-09-28, by wenzelm
tuned;
2001-09-28, by wenzelm
tuned;
2001-09-28, by wenzelm
- Exchanged % and %%.
2001-09-28, by berghofe
- Tuned syntax
2001-09-28, by berghofe
- Exchanged % and %%
2001-09-28, by berghofe
Exchanged % and %%.
2001-09-28, by berghofe
HOL: eliminated global items;
2001-09-27, by wenzelm
updated;
2001-09-27, by wenzelm
eliminated theories "equalities" and "mono" (made part of "Typedef",
2001-09-27, by wenzelm
renamed theory "subset" to "Typedef";
2001-09-27, by wenzelm
unsymbolize;
2001-09-27, by wenzelm
renamed "()" to Unity;
2001-09-27, by wenzelm
HOLogic.unit;
2001-09-27, by wenzelm
made unit type local;
2001-09-27, by wenzelm
tuned:
2001-09-27, by wenzelm
renamed "()" to Unity, made local;
2001-09-27, by wenzelm
added surjE;
2001-09-27, by wenzelm
prepared for Isabelle2001;
2001-09-27, by wenzelm
renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;
2001-09-27, by wenzelm
updated;
2001-09-27, by wenzelm
renamed real_of_int_eq_iff to real_of_int_inject;
2001-09-27, by wenzelm
document setup;
2001-09-27, by wenzelm
new-style theory;
2001-09-27, by wenzelm
Square roots of primes are irrational;
2001-09-27, by wenzelm
AddXIs [dvdI]; AddXEs [dvdE];
2001-09-27, by wenzelm
tuned;
2001-09-27, by wenzelm
tuned;
2001-09-27, by wenzelm
tuned;
2001-09-27, by wenzelm
AddXEs [UnI1, UnI2];
2001-09-27, by wenzelm
AddXEs [disjI1, disjI2];
2001-09-27, by wenzelm
ex/Hilbert_Classical.thy ex/document/root.tex;
2001-09-27, by wenzelm
tuned;
2001-09-27, by wenzelm
document setup;
2001-09-27, by wenzelm
derive tertium-non-datur by means of Hilbert's choice operator;
2001-09-27, by wenzelm
obsolete;
2001-09-27, by wenzelm
updated;
2001-09-27, by wenzelm
-v option;
2001-09-27, by wenzelm
verbose option;
2001-09-27, by wenzelm
use_dir: verbose option;
2001-09-27, by wenzelm
removed option -d (now standard behaviour);
2001-09-27, by wenzelm
option -v;
2001-09-27, by wenzelm
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
2001-09-26, by wenzelm
updated;
2001-09-26, by wenzelm
tuned order;
2001-09-26, by wenzelm
bold symbols;
2001-09-26, by wenzelm
tuned;
2001-09-26, by wenzelm
turn bullet into bold cdot (looks much better in printed output);
2001-09-26, by wenzelm
use darkblue for all links;
2001-09-26, by wenzelm
updated;
2001-09-26, by wenzelm
updated;
2001-09-25, by wenzelm
*** empty log message ***
2001-09-25, by wenzelm
tuned;
2001-09-25, by wenzelm
Minor improvements, added Example
2001-09-21, by oheimb
tuned;
2001-09-17, by wenzelm
Fixed proof term bug in permute_prems.
2001-09-13, by berghofe
result_error_default: include msg;
2001-09-12, by wenzelm
*** empty log message ***
2001-09-11, by nipkow
marginally improved comments
2001-09-10, by oheimb
corrected antiquotations in comment
2001-09-10, by oheimb
simplified vnam/vname, introduced fname, improved comments
2001-09-10, by oheimb
tuned usage;
2001-09-10, by wenzelm
print_state: subgoals;
2001-09-08, by wenzelm
export pretty_goals;
2001-09-08, by wenzelm
result_error_default: output *single* error message;
2001-09-08, by wenzelm
tuned;
2001-09-08, by wenzelm
ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);
2001-09-08, by wenzelm
* system: support Poly/ML 4.1.1 (large heaps);
2001-09-08, by wenzelm
smart selection of isabelle-process versus isabelle-interface;
2001-09-08, by wenzelm
renamed "antecedent" case to "rule_context";
2001-09-04, by wenzelm
*** empty log message ***
2001-09-04, by nipkow
*** empty log message ***
2001-09-03, by nipkow
tuned;
2001-09-01, by wenzelm
final proofs := 0;
2001-09-01, by wenzelm
HOL-Real-Hyperreal made a plain session (no longer an image);
2001-09-01, by wenzelm
renamed `keep_derivs' to `proofs', and made an integer;
2001-09-01, by wenzelm
* Proof General keywords specification is now part of the Isabelle
2001-08-31, by wenzelm
proper use of invent_names;
2001-08-31, by wenzelm
fixed header;
2001-08-31, by wenzelm
tuned headers;
2001-08-31, by wenzelm
keyword classification tables for Isabelle/Isar Proof General
2001-08-31, by wenzelm
New code generators for HOL.
2001-08-31, by berghofe
Initial revision of tools for proof terms.
2001-08-31, by berghofe
Added new option for setting level of detail for proof objects.
2001-08-31, by berghofe
Proof of True_implies_equals is stored with "open" derivation to
2001-08-31, by berghofe
Added code generator setup.
2001-08-31, by berghofe
Added new files for code generator.
2001-08-31, by berghofe
Renamed functions % and %% to avoid clash with syntax for proof terms.
2001-08-31, by berghofe
Adapted to new proof terms.
2001-08-31, by berghofe
Exported ml_reserved.
2001-08-31, by berghofe
Made consts list operations a bit faster.
2001-08-31, by berghofe
Added new argument to use_dir for derivation kind.
2001-08-31, by berghofe
Removed tag_assumption.
2001-08-31, by berghofe
Tuned naming of theorems.
2001-08-31, by berghofe
Added functions for printing primitive proof terms.
2001-08-31, by berghofe
Tuned function extend_lexicon.
2001-08-31, by berghofe
Initial revision of tools for proof terms.
2001-08-31, by berghofe
Now obsolete; replaced by LF style proof terms.
2001-08-31, by berghofe
Initial version of generic code generator.
2001-08-31, by berghofe
New implementation of LF style proof terms.
2001-08-31, by berghofe
Replaced old derivations by proof terms.
2001-08-31, by berghofe
Tidied function SELECT_GOAL.
2001-08-31, by berghofe
Added equality axioms and initialization of proof term package.
2001-08-31, by berghofe
Added setup for code generator.
2001-08-31, by berghofe
Added function unique_strings.
2001-08-31, by berghofe
- exported SAME exception
2001-08-31, by berghofe
Some basic rules are now stored with "open" derivations, to facilitate
2001-08-31, by berghofe
Added new files for proof terms.
2001-08-31, by berghofe
generated by Session.name;
2001-08-30, by wenzelm
export name;
2001-08-30, by wenzelm
cosmetics
2001-08-30, by oheimb
removed imname, uncurried Meth
2001-08-30, by oheimb
avoid ML bindings;
2001-08-29, by wenzelm
Implemented indentation schema for conditional rewrite trace.
2001-08-28, by nipkow
Traced depth of conditional rewriting
2001-08-23, by nipkow
tuned error message;
2001-08-21, by wenzelm
prefer immediate monos;
2001-08-16, by wenzelm
support for absolute namespace entry paths;
2001-08-15, by wenzelm
Updated proofs to take advantage of additional theorems proved by "typedef"
2001-08-10, by paulson
removed obsolete "arities";
2001-08-09, by wenzelm
tuned;
2001-08-09, by wenzelm
corrected initialization of locals, streamlined Impl
2001-08-09, by oheimb
corrected semantics of [iff] concerning rules with premises
2001-08-09, by oheimb
replaced 1 by 1'
2001-08-09, by oheimb
revisions and indexing
2001-08-09, by paulson
added pair_imageI (also as intro rule)
2001-08-09, by oheimb
renamed addaltern to addafter, addSaltern to addSafter
2001-08-09, by oheimb
added constify_ast_tr;
2001-08-08, by wenzelm
field_name_ast_tr superceded by constify_ast_tr in Pure;
2001-08-08, by wenzelm
_constify;
2001-08-08, by wenzelm
constify numeral tokens in order to allow translations;
2001-08-08, by wenzelm
* HOL: syntax translations now work properly with numerals and records
2001-08-08, by wenzelm
layout, subscripts
2001-08-08, by oheimb
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
2001-08-08, by wenzelm
polyml-4.1.1;
2001-08-08, by wenzelm
Hilbert_Choice is needed only in Main itself
2001-08-08, by paulson
Main is the proper parent of IOA
2001-08-08, by paulson
get it working again using Hilbert_Choice
2001-08-08, by paulson
Getting it working again with 1' instead of 1
2001-08-08, by paulson
new ZF/UNITY theory
2001-08-08, by paulson
*** empty log message ***
2001-08-08, by wenzelm
changed to full expressions with side effects
2001-08-08, by oheimb
changed to full expressions with side effects
2001-08-08, by oheimb
tuned;
2001-08-07, by wenzelm
tuned;
2001-08-07, by wenzelm
fix problem with user translations by making field names appear as consts;
2001-08-07, by wenzelm
tuned;
2001-08-07, by wenzelm
- Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
2001-08-07, by berghofe
Eliminated dependency of Funs_rangeE on SOME.
2001-08-07, by berghofe
removed the warning from [iff]
2001-08-07, by oheimb
Tweaks for 1 -> 1'
2001-08-07, by paulson
Converted 1 to 1'
2001-08-06, by paulson
1 -> 1'
2001-08-06, by nipkow
Changed 1 to 1' (= Suc 0)
2001-08-06, by paulson
turned translation for 1::nat into def.
2001-08-06, by nipkow
three new theorems
2001-08-06, by paulson
removed the warning from [iff]
2001-08-06, by paulson
removed an unsuitable default simprule
2001-08-06, by paulson
tidying and moving the theorem "choice"
2001-08-06, by paulson
new result comp_surj
2001-08-06, by paulson
numerous stylistic changes and indexing
2001-08-03, by paulson
additional revisions to chapters 1, 2
2001-07-26, by paulson
revisions and indexing
2001-07-26, by paulson
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
2001-07-25, by paulson
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-07-25, by paulson
partial restructuring to reduce dependence on Axiom of Choice
2001-07-25, by paulson
removed reference to Ex_def
2001-07-25, by paulson
partial restructuring to reduce dependence on Axiom of Choice
2001-07-25, by paulson
tweaks and indexing
2001-07-24, by paulson
cosmetics
2001-07-23, by oheimb
Final version of Florian Kammueller's examples
2001-07-23, by paulson
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23, by paulson
improved version of the Pi-theorems
2001-07-23, by paulson
PiSets moved to GroupTheory, while LocaleGroup deleted
2001-07-23, by paulson
live links
2001-07-23, by paulson
The final version of Florian Kammueller's proofs
2001-07-23, by paulson
slight improvement for iff attribute
2001-07-23, by oheimb
replaced SOME by THE;
2001-07-22, by wenzelm
the_equality [intro];
2001-07-22, by wenzelm
tuned;
2001-07-22, by wenzelm
declare trans [trans] (*overridden in theory Calculation*);
2001-07-22, by wenzelm
HOL: added "The";
2001-07-20, by wenzelm
private "myinv" (uses "The" instead of "Eps");
2001-07-20, by wenzelm
replaced "Eps" by "The";
2001-07-20, by wenzelm
HOL_ss: the_eq_trivial, the_sym_eq_trivial;
2001-07-20, by wenzelm
tuned;
2001-07-20, by wenzelm
added "The" (definite description operator) (by Larry);
2001-07-20, by wenzelm
*** empty log message ***
2001-07-20, by wenzelm
SEDINDEX = ./isa-index;
2001-07-20, by wenzelm
tidying the index
2001-07-17, by paulson
tidying the index
2001-07-17, by paulson
indexing
2001-07-16, by paulson
abtract non-emptiness statements (no longer use Eps);
2001-07-15, by wenzelm
tuned;
2001-07-15, by wenzelm
working
2001-07-13, by paulson
oops
2001-07-13, by paulson
fixed bad error in tdxbold; also removed default indexing in \\rulename
2001-07-13, by paulson
tweaks
2001-07-13, by paulson
added\\protect
2001-07-13, by paulson
more indexing
2001-07-13, by paulson
indexing tweaks
2001-07-13, by paulson
less indexing of theorem names
2001-07-13, by paulson
indexing
2001-07-13, by paulson
contrapos_pn
2001-07-13, by paulson
index file
2001-07-13, by paulson
removed a4paper
2001-07-12, by paulson
more in the Springer style
2001-07-12, by paulson
indexing
2001-07-12, by paulson
indexing
2001-07-11, by paulson
messages, and proper treatment of footnotes
2001-07-11, by paulson
new preface
2001-07-11, by paulson
tweaks for new version
2001-07-11, by paulson
indexing and tweaks
2001-07-11, by paulson
tweak
2001-07-11, by paulson
careful changes to make its output identical to that of indexing macros
2001-07-11, by paulson
new macro file for the tutorial
2001-07-11, by paulson
separate preface and macro file
2001-07-11, by paulson
do not remove Rules and Sets TeX files
2001-07-11, by paulson
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip