Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-1536
+1536
+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.
*** 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
isa-index replaces ../sedindex: knows about \\isa
2001-07-09, by paulson
two Isar tactic scripts
2001-07-06, by paulson
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
2001-07-03, by wenzelm
GroupTheory
2001-07-03, by paulson
new lemmas
2001-07-03, by paulson
better treatment of restrict (lam)
2001-07-03, by paulson
Locale-based group theory proofs
2001-07-03, by paulson
ppc-darwin;
2001-07-02, by wenzelm
do *not* ./configure;
2001-07-02, by wenzelm
#!/usr/bin/env bash;
2001-07-02, by wenzelm
...
2001-07-02, by wenzelm
the records section
2001-06-29, by paulson
the records section
2001-06-29, by paulson
for the records section
2001-06-29, by paulson
a few new and/or improved results
2001-06-26, by paulson
gave Greatest_le its proper name
2001-06-26, by paulson
resolved name clash
2001-06-26, by paulson
tidied
2001-06-26, by paulson
now more like the HOL versions, and with the Square Root example added
2001-06-26, by paulson
tidying and consolidating files
2001-06-26, by paulson
tidying and consolidating files
2001-06-26, by paulson
removed duplicate proof and small mod.
2001-06-26, by nipkow
Simprocs for type "nat" no longer introduce numerals unless
2001-06-25, by paulson
Simprocs for type "nat" no longer introduce numerals unless they are already
2001-06-25, by paulson
added NanoJava
2001-06-16, by oheimb
tidied
2001-06-13, by paulson
New proof of gcd_zero after a change to Divides.ML made the old one fail
2001-06-13, by paulson
a couple of new theorems
2001-06-13, by paulson
corrected xsymbol/HTML syntax
2001-06-12, by oheimb
Fixed bug in function rebuild.
2001-06-11, by berghofe
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
2001-06-10, by paulson
tuned
2001-06-09, by wenzelm
tuned Primes theory;
2001-06-09, by wenzelm
addition of the GREATEST quantifier
2001-06-09, by paulson
renaming of evs in the Fake rule
2001-06-09, by paulson
new material from the Sylow proof
2001-06-09, by paulson
simplified a proof using new dvd rules
2001-06-09, by paulson
moved Primes.thy from NumberTheory to Library
2001-06-09, by paulson
Removed BCV
2001-06-08, by nipkow
*** empty log message ***
2001-06-05, by nipkow
This is now superseded by MicroJava/BV
2001-06-05, by nipkow
renamed # to ## to avoid clashing with List cons
2001-06-01, by paulson
now checks for leading meta-quantifiers and complains, instead of
2001-06-01, by paulson
tuned
2001-05-31, by wenzelm
added HOL-CTL;
2001-05-31, by wenzelm
tuned
2001-05-31, by wenzelm
examples files start from Main instead of various ZF theories
2001-05-31, by paulson
invent_names
2001-05-31, by wenzelm
added HOL-CTL example;
2001-05-31, by bauerg
added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31, by oheimb
added FOCUS including the One-Element Buffer by Manfred Broy
2001-05-31, by oheimb
added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31, by oheimb
added stream length, map, and filter
2001-05-31, by oheimb
corrected ML names of definitions, added chain_shift
2001-05-31, by oheimb
corrected ML names of definitions
2001-05-31, by oheimb
improved iff_add_global, new function add_rules factoring out common behaviour
2001-05-31, by oheimb
streamlined addIffs/delIffs, added warnings
2001-05-31, by oheimb
replaced Sel_injective_cprod by new injective_fst_snd
2001-05-31, by oheimb
added lub_range_mono and lub_range_shift
2001-05-31, by oheimb
added chain_monofun
2001-05-31, by oheimb
added same_fstI as safe intro rule
2001-05-31, by oheimb
added injective_fst_snd
2001-05-31, by oheimb
added nat_not_singleton (also to simpset)
2001-05-31, by oheimb
added Least_Suc2
2001-05-31, by oheimb
added list_all2_trans
2001-05-31, by oheimb
added weak_coinduct_image
2001-05-31, by oheimb
Allow Suc-numerals as coefficients in lin-arith formulae
2001-05-31, by nipkow
corrected entry for iff attribute
2001-05-31, by oheimb
extended doc for iff attribute
2001-05-30, by oheimb
injectivity of ^;
2001-05-30, by bauerg
deleted a needless reference to rtrancl_unfold
2001-05-29, by paulson
improved handling of space before/after parentheses
2001-05-28, by oheimb
Inductive characterization of wfrec combinator.
2001-05-22, by berghofe
Transitive closure is now defined via "inductive".
2001-05-22, by berghofe
Representing set for type nat is now defined via "inductive".
2001-05-22, by berghofe
Inductive definitions are now introduced earlier in the theory hierarchy.
2001-05-22, by berghofe
nat_diff_split_asm, for the assumptions
2001-05-22, by paulson
if_splits and split_if_asm
2001-05-21, by paulson
fixed the X-symbol syntax for lambda
2001-05-21, by paulson
the rest of integer division
2001-05-21, by paulson
X-symbols for set theory
2001-05-21, by paulson
X-symbols for ZF
2001-05-21, by paulson
X-symbols for ZF
2001-05-21, by paulson
X-symbols for set theory
2001-05-21, by paulson
X-symbols for set theory
2001-05-21, by paulson
Division examples
2001-05-21, by paulson
ZF: division
2001-05-21, by paulson
new theorem dvd_mult_right
2001-05-20, by paulson
added (no)_type_brackets
2001-05-20, by nipkow
power_le_dvd replaces power_less_dvd
2001-05-19, by paulson
spelling check
2001-05-19, by paulson
minor suggestions by Tanja Vos
2001-05-18, by paulson
*** empty log message ***
2001-05-18, by nipkow
*** empty log message ***
2001-05-18, by nipkow
added comments
2001-05-18, by nipkow
added ^ on functions.
2001-05-18, by nipkow
auto update
2001-05-17, by paulson
typo, etc.
2001-05-17, by paulson
minor revisons
2001-05-17, by paulson
spelling
2001-05-16, by paulson
typo
2001-05-16, by paulson
welltyping -> wt_step
2001-05-16, by nipkow
simplified defs and proofs a little
2001-05-14, by nipkow
mult_Suc generally, not just for numerals.
2001-05-11, by nipkow
added mult_Suc laws to lin.arith.simpset.
2001-05-11, by nipkow
improved tracing of permutative rules.
2001-05-10, by nipkow
*** empty log message ***
2001-05-10, by nipkow
*** empty log message ***
2001-05-10, by nipkow
*** empty log message ***
2001-05-10, by nipkow
improved simproc trace IGNORED
2001-05-09, by nipkow
fixed comment
2001-05-08, by paulson
new takeWhile lemma
2001-05-08, by paulson
fixed a slow proof; tidied
2001-05-08, by paulson
conversion of Auth/TLS to Isar script
2001-05-08, by paulson
minor bugfix for AddIffs
2001-05-07, by oheimb
*** empty log message ***
2001-05-04, by nipkow
made same_fst recdef_simp
2001-05-04, by nipkow
improved EVERY'
2001-05-03, by oheimb
*** empty log message ***
2001-05-03, by nipkow
minor tweaks
2001-05-03, by paulson
minor tweaks
2001-05-03, by paulson
remove unnecessary TeX files
2001-05-03, by paulson
*** empty log message ***
2001-05-02, by nipkow
*** empty log message ***
2001-05-01, by nipkow
to ignore the *.class files that are copied here
2001-05-01, by paulson
new proof
2001-04-30, by nipkow
minor bugfix for subst_RS
2001-04-30, by oheimb
improve support for EVERY', added support for EVERY
2001-04-30, by oheimb
minor bugfix for newlines with Goalw
2001-04-30, by oheimb
added support for EVERY', improved support for RS
2001-04-30, by oheimb
better treatment of methods: uses Method.ctxt_args to refer to current
2001-04-27, by paulson
changes specifically for the book version
2001-04-25, by paulson
new reference: Yahalom
2001-04-24, by paulson
revisions to Protocols chapter
2001-04-24, by paulson
simplified proofs concerning class_rec
2001-04-24, by oheimb
removal of image_Collect as a default simprule
2001-04-24, by paulson
(rough) conversion of Auth/Recur to Isar format
2001-04-24, by paulson
added parentheses for 'b y' syntax, added primitive smp_tac support
2001-04-23, by oheimb
*** empty log message ***
2001-04-20, by nipkow
suggestions from OHeimb
2001-04-20, by paulson
renaming of theory LOmega to lomega2 in order to prevent a possible
2001-04-19, by paulson
*** empty log message ***
2001-04-19, by nipkow
polyml-4.1;
2001-04-18, by wenzelm
*** empty log message ***
2001-04-17, by nipkow
*** empty log message ***
2001-04-17, by nipkow
*** empty log message ***
2001-04-17, by paulson
TODO
2001-04-16, by wenzelm
proper order of order_less_asym';
2001-04-12, by wenzelm
cleanup, tuned
2001-04-12, by kleing
converted many HOL/Auth theories to Isar scripts
2001-04-12, by paulson
symlinks to ../../../HOL/Auth. Fingers crossed...
2001-04-11, by paulson
Protocols chapter
2001-04-10, by paulson
back to Unix format...
2001-04-10, by paulson
security protocol chapter
2001-04-10, by paulson
security protocol refs
2001-04-10, by paulson
new theorem Fake_parts_insert_in_Un
2001-04-09, by paulson
extra display
2001-04-09, by paulson
*** empty log message ***
2001-04-09, by paulson
lexicographic product of two relations: updated HOL.tex
2001-04-09, by paulson
Isar hint
2001-04-09, by paulson
thm output: Attrib.local_thmss;
2001-04-07, by wenzelm
tuned
2001-04-07, by wenzelm
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
quantifier instantiation
2001-03-30, by paulson
the one-point rule for bounded quantifiers
2001-03-30, by paulson
generalization of 1 point rules for ALL
2001-03-29, by nipkow
*** empty log message ***
2001-03-29, by nipkow
misc tidying; changing the predicate isSymKey to the set symKeys
2001-03-29, by paulson
Got rid of is_dfa
2001-03-28, by nipkow
MicroJava/BV dependencies incomplete
2001-03-28, by nipkow
fixed bug in tactic for ball 1 point simproc
2001-03-27, by nipkow
Vos
2001-03-27, by paulson
simplified proofs
2001-03-26, by nipkow
simplified proofs
2001-03-26, by nipkow
I forgot a few bases cases for the 1-point rules...
2001-03-26, by nipkow
shortening and streamlining of proofs
2001-03-23, by paulson
added simproc for bounded quantifiers
2001-03-23, by nipkow
added one point simprocs for bounded quantifiers
2001-03-23, by nipkow
new theorem analz_Decrypt'
2001-03-22, by paulson
new theorem analz_isSymKey_Decrypt
2001-03-22, by paulson
some X-symbols
2001-03-22, by paulson
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by paulson
translations: a tweak
2001-03-15, by paulson
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-14, by nipkow
*** empty log message ***
2001-03-14, by nipkow
minor tuning
2001-03-14, by paulson
*** empty log message ***
2001-03-13, by nipkow
*** empty log message ***
2001-03-12, by nipkow
*** empty log message ***
2001-03-12, by nipkow
arith_tac now copes with propositional reasoning as well.
2001-03-09, by nipkow
expanded abbrevs
2001-03-07, by paulson
added strange 'b y' syntax
2001-03-07, by streckem
*** empty log message ***
2001-03-07, by nipkow
*** empty log message ***
2001-03-07, by nipkow
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
a few basic X-symbols
2001-03-05, by paulson
conversion of Message.thy to Isar format
2001-03-02, by paulson
*** empty log message ***
2001-03-02, by ehmety
conversion of Message.thy to Isar format
2001-03-02, by paulson
streamlined a proof
2001-03-02, by paulson
auto-update
2001-02-28, by paulson
*** empty log message ***
2001-02-27, by nipkow
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
2001-02-27, by paulson
kildall now via while and therefore executable!
2001-02-27, by nipkow
minor tweaks to speed the proofs
2001-02-26, by paulson
minor fixes
2001-02-26, by paulson
renamed addaltern to addafter, addSaltern to addSafter
2001-02-23, by oheimb
removed performance leak for split_conv_tac (and corresponding safe wrapper)
2001-02-23, by oheimb
subst method and a new section on rule, rule_tac, etc
2001-02-22, by paulson
removed unused constant
2001-02-22, by kleing
removed unused function
2001-02-22, by kleing
a PROPER tidy-up
2001-02-22, by paulson
recoded function iter with the help of the while-combinator.
2001-02-22, by nipkow
revisions in response to comments by Tobias
2001-02-21, by paulson
revisions in response to comments by Tobias
2001-02-21, by paulson
added split_conv_tac (also to claset()) as an optimization
2001-02-21, by oheimb
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-20, by oheimb
simplified proofs for splitI and splitD, added splitD'
2001-02-20, by oheimb
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-20, by oheimb
corrected comments on addbefore and addSbefore
2001-02-20, by oheimb
added same_fstI
2001-02-20, by oheimb
simplified definition of wrapper bspec
2001-02-20, by oheimb
added image_cong to default congs of recdef
2001-02-20, by oheimb
added add_arith (just as hint by now)
2001-02-20, by oheimb
added rearrange_prems
2001-02-20, by oheimb
debugging: replaced gen_all by forall_elim_vars_safe
2001-02-20, by oheimb
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-17, by nipkow
fixed the obvious errors Tobias found
2001-02-16, by paulson
Least_def now refers to LeastM
2001-02-16, by paulson
for the change to LEAST
2001-02-16, by paulson
Blast bug fix made old proof too slow
2001-02-16, by paulson
Blast bug fix: now always duplicates when applying a haz rule,
2001-02-16, by paulson
Blast bug fix made old proof too slow
2001-02-16, by paulson
Streamlining for the bug fix in Blast.
2001-02-16, by paulson
*** empty log message ***
2001-02-16, by nipkow
*** empty log message ***
2001-02-16, by nipkow
*** empty log message ***
2001-02-16, by nipkow
tuned;
2001-02-16, by wenzelm
eliminate get_def;
Isabelle99-2
2001-02-15, by wenzelm
tuned;
2001-02-15, by wenzelm
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
moved inv_image to Relation
2001-02-15, by oheimb
supressed some warnings on identical proofstate
2001-02-15, by oheimb
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
2001-02-15, by oheimb
simplified proof of Least_mono
2001-02-15, by oheimb
added wellorder axclass
2001-02-15, by oheimb
moved inv_image to Relation
2001-02-15, by oheimb
moved wf_less from Nat.ML to NatDef.ML
2001-02-15, by oheimb
added nat as instance of new wellorder axclass
2001-02-15, by oheimb
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
added trial proof
2001-02-15, by oheimb
improved subst_RS
2001-02-15, by oheimb
added missiong word
2001-02-15, by oheimb
*** empty log message ***
2001-02-15, by nipkow
index mod syntax;
2001-02-15, by wenzelm
tuned;
2001-02-14, by wenzelm
isatool install -k;
2001-02-14, by wenzelm
handle KDE version 1 or 2;
2001-02-14, by wenzelm
isatool install handles KDE version 1 or 2;
2001-02-14, by wenzelm
removed whitespace
2001-02-14, by oheimb
supressed some warnings on identical proofstate
2001-02-14, by oheimb
adhoc script for creating complete Isabelle dist pages;
2001-02-14, by wenzelm
imp_cong2 -> imp_cong
2001-02-14, by berghofe
new function get_overloads
2001-02-14, by paulson
updated the unicity proof
2001-02-14, by paulson
tidying
2001-02-14, by paulson
not_bad_tac is obsolete
2001-02-14, by paulson
a new theorem from Bryan Ford
2001-02-14, by paulson
added support for AddXIs, AddXEs, AddXDs
2001-02-14, by oheimb
tuned;
2001-02-14, by wenzelm
tuned;
2001-02-13, by wenzelm
tuned;
2001-02-13, by wenzelm
\remarksfalse;
2001-02-13, by wenzelm
tuned;
2001-02-13, by wenzelm
swapped Fleuriot and Paulson
2001-02-13, by paulson
create dist packages;
2001-02-13, by wenzelm
partial conversion to Isar script style in HOL/Auth removes some .ML files
2001-02-13, by paulson
partial conversion to Isar script style in HOL/Auth removes some .ML files
2001-02-13, by paulson
partial conversion to Isar script style
2001-02-13, by paulson
tuned;
2001-02-13, by wenzelm
tuned;
2001-02-12, by wenzelm
support \<subseteq> syntax in classes/classrel/axclass/instance;
2001-02-12, by wenzelm
\<subseteq> syntax for classes/classrel/axclass/instance;
2001-02-12, by wenzelm
\<subseteq>;
2001-02-12, by wenzelm
added "xsymbols" syntax for "=?=";
2001-02-11, by wenzelm
more robust selection of calculational rules;
2001-02-11, by wenzelm
tuned trans rules;
2001-02-11, by wenzelm
updated;
2001-02-11, by wenzelm
tuned;
2001-02-11, by wenzelm
Changes to HOL/Algebra:
2001-02-10, by ballarin
Definition of setsum (sort constraint) relaxed to {zero, plus}.
2001-02-10, by ballarin
Updates to HOL/Algebra:
2001-02-10, by ballarin
tuned;
2001-02-09, by wenzelm
lower priority for forw_subst;
2001-02-09, by wenzelm
tuned;
2001-02-09, by wenzelm
not used any more (all Isar style)
2001-02-09, by kleing
removed MicroJava/Digest.thy
2001-02-09, by kleing
tuned for 99-2 release
2001-02-09, by kleing
unsymbolized;
2001-02-09, by wenzelm
tuned;
2001-02-07, by wenzelm
improved;
2001-02-07, by wenzelm
solved non-initialization problems; improvements using prefer
2001-02-07, by oheimb
various revisions in response to comments from Tobias
2001-02-07, by paulson
val get_goal: state -> context * (thm list * thm);
2001-02-07, by wenzelm
4.0 version;
2001-02-06, by wenzelm
snapshot of a new version
2001-02-06, by paulson
new theorem Transset_iff_Union_subset
2001-02-06, by paulson
tuned
2001-02-06, by kleing
improved;
2001-02-05, by wenzelm
polyml multiplatform setup;
2001-02-05, by wenzelm
tuned
2001-02-05, by wenzelm
tuned;
2001-02-05, by wenzelm
improved document (added headers etc)
2001-02-05, by oheimb
tuned
2001-02-05, by wenzelm
improvements concerning instantiations etc.
2001-02-05, by oheimb
disable non-existant chapters
2001-02-05, by wenzelm
tuned;
2001-02-05, by wenzelm
fixed version string;
2001-02-05, by wenzelm
polyml-3.x.ML vs polyml-4.0.ML;
2001-02-05, by wenzelm
renamed polyml.ML to polyml-3.x.ML and polyml-4.0.ML to polyml.ML (default);
2001-02-05, by wenzelm
tuned;
2001-02-05, by wenzelm
example Proof General settings;
2001-02-05, by wenzelm
document setup;
2001-02-04, by wenzelm
converted to new-style;
2001-02-04, by wenzelm
moved theory Perm to HOL/Library;
2001-02-04, by wenzelm
added no_document
2001-02-04, by wenzelm
tuned
2001-02-04, by wenzelm
added Permutation;
2001-02-04, by wenzelm
moved from Induct/ to Library/
2001-02-04, by wenzelm
updated
2001-02-04, by wenzelm
added no_document;
2001-02-04, by wenzelm
updated split_format;
2001-02-04, by wenzelm
* no_document ML operator temporarily disables LaTeX document
2001-02-04, by wenzelm
HOL-NumberTheory: converted to new-style format and proper document setup;
2001-02-04, by wenzelm
tuned msg;
2001-02-03, by wenzelm
tuned;
2001-02-03, by wenzelm
Induct: converted some theories to new-style format;
2001-02-03, by wenzelm
fixed syntax of 'split_format';
2001-02-03, by wenzelm
use fgrep;
2001-02-03, by wenzelm
HOL: inductive package no longer splits induction rule aggressively,
2001-02-03, by wenzelm
commutation theory, ported by Sidi Ehmety
2001-02-03, by paulson
updated;
2001-02-03, by wenzelm
simplified 'split_format' syntax;
2001-02-03, by wenzelm
'split_format' attribute;
2001-02-02, by wenzelm
tuned;
2001-02-02, by wenzelm
module setup;
2001-02-02, by wenzelm
use hol_simplify;
2001-02-02, by wenzelm
use hol_rewrite_cterm;
2001-02-02, by wenzelm
added hol_simplify, hol_rewrite_cterm;
2001-02-02, by wenzelm
split = split_conv (for compatibility);
2001-02-02, by wenzelm
added hidden internal_split constant;
2001-02-02, by wenzelm
isatool convert;
2001-02-02, by wenzelm
new theorem fib_mult_eq_setsum
2001-02-02, by paulson
little bugfixes; added induct_thm_tac
2001-02-02, by oheimb
moved to Product_Type_lemmas.ML
2001-02-01, by wenzelm
added translations for bind_thm and val
2001-02-01, by oheimb
converted to Isar, simplifying recursion on class hierarchy
2001-02-01, by oheimb
converted to Isar therory, adding attributes complete_split and split_format
2001-02-01, by oheimb
converted to new-style theories;
2001-02-01, by wenzelm
updated
2001-02-01, by wenzelm
ext_classrel: certify_class;
2001-02-01, by wenzelm
comment
2001-02-01, by wenzelm
tuned
2001-02-01, by wenzelm
tuned;
2001-02-01, by wenzelm
added "numerals" theorems;
2001-02-01, by wenzelm
thms_containing: term args;
2001-02-01, by wenzelm
* Pure: 'thms_containing' now takes actual terms as arguments;
2001-02-01, by wenzelm
added sum_case_map_upd_empty, sum_case_empty_map_upd, and
2001-02-01, by oheimb
debugged declare
2001-02-01, by oheimb
further minor improvements
2001-02-01, by oheimb
strip_blanks moved to General/symbol.ML;
2001-01-31, by wenzelm
pretty_text: tweak_lines handles linebreaks gracefully;
2001-01-31, by wenzelm
added strip_blanks;
2001-01-31, by wenzelm
added attribute declarations, etc.
2001-01-31, by oheimb
improved theory reference in comment
2001-01-31, by oheimb
added diff_single_insert and subset_image_iff
2001-01-31, by oheimb
shortened proof of some1_equality
2001-01-31, by oheimb
more robust handling of rule cases hints;
2001-01-31, by wenzelm
tuned;
2001-01-30, by wenzelm
added if_def2
2001-01-30, by oheimb
added foldln
2001-01-30, by oheimb
corrected file name suffixes
2001-01-30, by oheimb
removed (obsolete) mult_assumption
2001-01-30, by oheimb
Fixed bug in complete_split_rule_var.
2001-01-30, by berghofe
tuned;
2001-01-30, by wenzelm
avoid dead code;
2001-01-29, by wenzelm
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
2001-01-29, by nipkow
*** empty log message ***
2001-01-29, by nipkow
*** empty log message ***
2001-01-29, by nipkow
added Unix example;
2001-01-29, by wenzelm
updated;
2001-01-29, by wenzelm
*** empty log message ***
2001-01-29, by wenzelm
Completely split rule eval_evals_exec.induct before applying it.
2001-01-29, by berghofe
New function complete_split_rule for complete splitting of partially
2001-01-29, by berghofe
Splitting of arguments of product types in induction rules is now less
2001-01-29, by berghofe
fixed the pr example
2001-01-29, by paulson
simplified gcd
2001-01-29, by paulson
fixed set comprehension print translation
2001-01-28, by nipkow
Merged Example into While_Combi
2001-01-26, by nipkow
*** empty log message ***
2001-01-26, by nipkow
renamed to Transitive_Closure_lemmas.ML;
2001-01-26, by wenzelm
tuned;
2001-01-26, by wenzelm
Transitive_Closure turned into new-style theory;
2001-01-26, by wenzelm
tuned;
2001-01-26, by wenzelm
*** empty log message ***
2001-01-25, by nipkow
added Martin Strecker, Christian Buttenberg, Alexandra Kirsch and project
2001-01-25, by kleing
* Document preparation: renamed standard symbols \<ll> to \<lless> and
2001-01-24, by wenzelm
added eufrak symbols;
2001-01-24, by wenzelm
more symbols;
2001-01-24, by wenzelm
empty_upd_none;
2001-01-24, by wenzelm
debugging and extensions
2001-01-24, by oheimb
*** empty log message ***
2001-01-24, by nipkow
*** empty log message ***
2001-01-24, by nipkow
no_brackets;
2001-01-24, by wenzelm
tuned;
2001-01-23, by wenzelm
arg_cong, tacticals, pr, defer, prefer
2001-01-23, by paulson
added HOL-Unix example;
2001-01-23, by wenzelm
2 to #2
2001-01-23, by paulson
the 0<n premise was unnecessary
2001-01-23, by paulson
added a "pr" example; tidied
2001-01-23, by paulson
deleted several obsolete lemmas from NatArith.ML
2001-01-22, by paulson
tidied using arith_tac
2001-01-22, by paulson
deleted obsolete theorems
2001-01-22, by paulson
tided
2001-01-22, by paulson
arg_cong example; tidying to use @subgoals
2001-01-22, by paulson
rename_tac example; tidying to use @subgoals
2001-01-22, by paulson
new examples theory Rules/Tacticals.thy
2001-01-22, by paulson
setuo indent: \isaindent;
2001-01-21, by wenzelm
setup indent;
2001-01-21, by wenzelm
added spaces;
2001-01-21, by wenzelm
support general indentation (e.g. for non-tt latex output);
2001-01-21, by wenzelm
added replicate_string;
2001-01-21, by wenzelm
updated;
2001-01-21, by wenzelm
\isaindent;
2001-01-21, by wenzelm
tuned;
2001-01-20, by wenzelm
Ring_and_Field_Example;
2001-01-20, by wenzelm
instance int :: ordered_ring moved to Ring_and_Field_Example, because
2001-01-20, by wenzelm
added Library/Ring_and_Field_Example.thy;
2001-01-20, by wenzelm
*** empty log message ***
2001-01-20, by wenzelm
added HOL/Library/Nested_Environment.thy;
2001-01-19, by wenzelm
updated;
2001-01-19, by wenzelm
more bugs;
2001-01-19, by wenzelm
forget RPM;
2001-01-19, by wenzelm
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
2001-01-19, by wenzelm
made SML/XL happy;
2001-01-18, by wenzelm
tuned;
2001-01-18, by wenzelm
show(_i): check goal;
2001-01-18, by wenzelm
show/thus: check_goal;
2001-01-18, by wenzelm
show/thus: Toplevel.proof';
2001-01-18, by wenzelm
infix \\\\;
2001-01-18, by wenzelm
added exists_stamp;
2001-01-18, by wenzelm
use Sign.PureN, Sign.CPureN;
2001-01-18, by wenzelm
Sign.exists_stamp;
2001-01-18, by wenzelm
tuned \<And> and \<Or>;
2001-01-18, by wenzelm
generate index.html for pdf docs;
2001-01-18, by wenzelm
splitted Loop rule
2001-01-18, by oheimb
removed redundant proof
2001-01-18, by paulson
is_class and class now as defs (rather than translations); corrected Digest.thy
2001-01-18, by oheimb
use_output: proper handling of non-ASCII symbols;
2001-01-16, by wenzelm
export plain_output;
2001-01-16, by wenzelm
Store.thy is obsolete (newref isn't used any more)
2001-01-16, by kleing
removed obsolete MicroJava/JVM/Store.thy
2001-01-16, by kleing
newref -> new_Addr
2001-01-16, by kleing
renamings: real_of_nat, real_of_int -> (overloaded) real
2001-01-16, by paulson
renamed Product_Type.split to split_conv;
2001-01-16, by wenzelm
use Syntax.read_xnum;
2001-01-16, by wenzelm
tuned examples;
2001-01-16, by wenzelm
* HOL/datatype: induction rule for arbitrarily branching datatypes is
2001-01-16, by wenzelm
use_text etc.: proper output of error messages;
2001-01-16, by wenzelm
export fold_ast etc.;
2001-01-16, by wenzelm
removed Session.finish ();
2001-01-16, by wenzelm
proper induction rule for arbitrarily branching datatype;
2001-01-16, by wenzelm
export inductive_forall_name, inductive_forall_def, rulify;
2001-01-16, by wenzelm
improved string syntax (allow translation rules);
2001-01-16, by wenzelm
renamed Abs_Node_inject to Abs_Node_inj;
2001-01-16, by wenzelm
added atomize_strip_tac;
2001-01-16, by wenzelm
tuned atomize;
2001-01-16, by wenzelm
-f option;
2001-01-16, by wenzelm
removed;
2001-01-16, by wenzelm
removed ex/StringEx.ML;
2001-01-16, by wenzelm
split_conv;
2001-01-16, by wenzelm
updated;
2001-01-16, by wenzelm
isabelle -f;
2001-01-16, by wenzelm
more method_setup examples;
2001-01-16, by wenzelm
lcp's pass over the book, chapters 1-8
2001-01-15, by paulson
removed instructions Aconst_null+Bipush, introduced LitPush
2001-01-14, by kleing
tuned
2001-01-14, by kleing
*** empty log message ***
2001-01-14, by nipkow
use_text_verbose: priority output;
2001-01-12, by wenzelm
use_mltext: priority output;
2001-01-12, by wenzelm
HOLogic.dest_binum;
2001-01-12, by wenzelm
hide dest_bin;
2001-01-12, by wenzelm
HOLogic.dest_binum;
2001-01-12, by wenzelm
wrong font for braces
2001-01-12, by paulson
LateX-2e moans about using \\choose
2001-01-12, by paulson
the \\epsilon character causes font errors in a section title
2001-01-12, by paulson
made SML/NJ happy;
2001-01-12, by wenzelm
lcp's pass over the book, chapters 1-8
2001-01-12, by paulson
renaming of some files
2001-01-12, by paulson
updated for new version of even-examples.tex
2001-01-12, by paulson
updated for new version of advanced-examples.tex
2001-01-12, by paulson
abs and other small changes
2001-01-12, by paulson
updated for new version of numerics.tex
2001-01-12, by paulson
renaming to avoid clashes
2001-01-12, by paulson
auto update
2001-01-12, by paulson
general revisions
2001-01-12, by paulson
added Sigma_Algebra;
2001-01-12, by wenzelm
added Induct/Sigma_Algebra.thy;
2001-01-12, by wenzelm
tuned;
2001-01-12, by wenzelm
do not hilite "xnum";
2001-01-11, by wenzelm
make_raw: do not AutoBind.drop_judgment;
2001-01-11, by wenzelm
induct cases: RuleCases.make_raw;
2001-01-11, by wenzelm
added strict_prefixI', strict_prefixE';
2001-01-11, by wenzelm
subst syntax;
2001-01-11, by wenzelm
*** empty log message ***
2001-01-11, by nipkow
lcp's suggestions for CTL
2001-01-11, by paulson
*** empty log message ***
2001-01-11, by nipkow
a new label
2001-01-11, by paulson
revisions corresponding to the new version of sets.tex
2001-01-11, by paulson
Added <cdot> syntax for continuous application $.
2001-01-10, by nipkow
isatool unsymbolize;
2001-01-10, by wenzelm
updated;
2001-01-10, by wenzelm
tuned \DOT, \DDOT;
2001-01-10, by wenzelm
added \<wrong> symbol;
2001-01-10, by wenzelm
tuned;
2001-01-10, by wenzelm
revisions e.g. images, transitive closure...
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
*** empty log message ***
2001-01-10, by nipkow
case_tac on bools
2001-01-10, by paulson
case_tac subgoals
2001-01-10, by paulson
deleted the obsolete nat_neqE (and reformatting)
2001-01-10, by paulson
deleted the obsolete nat_neqE
2001-01-10, by paulson
generalizing the LEAST theorems from "nat" to linear
2001-01-10, by paulson
now using "by" for one-line proofs
2001-01-10, by paulson
various changes including the SOME examples, rule_format and "by"
2001-01-10, by paulson
loads the new theory
2001-01-10, by paulson
reformatting, and splitting the end of "Primes" to create "Forward"
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
now using "by" for one-line proofs
2001-01-10, by paulson
introduction of "by" and a few examples of SOME
2001-01-10, by paulson
auto update
2001-01-10, by paulson
new wfrec example
2001-01-10, by paulson
fixed the treatment of Rules and Sets
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
use \<acute>;
2001-01-10, by wenzelm
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
2001-01-10, by wenzelm
added acute, cedilla, dieresis, hungarumlaut;
2001-01-09, by wenzelm
` -> $
2001-01-09, by nipkow
*** empty log message ***
2001-01-09, by nipkow
`` -> ` and ``` -> ``
2001-01-09, by nipkow
`` -> and ``` -> ``
2001-01-09, by nipkow
replaced \<macron> by \<inverse>;
2001-01-09, by wenzelm
avoid renaming of params in cases;
2001-01-09, by wenzelm
split_all operation;
2001-01-09, by wenzelm
improved evaluation judgment syntax; modified Loop rule
2001-01-09, by oheimb
syntax (xsymbols);
2001-01-09, by wenzelm
Removed Applyall
2001-01-08, by nipkow
additional pattern allows reduction of fractions to lowest terms
2001-01-08, by paulson
*** empty log message ***
2001-01-08, by nipkow
updated;
2001-01-07, by wenzelm
removed ID (avoid CVS conflicts with generated versions);
2001-01-07, by wenzelm
CHANGED_PROP;
2001-01-07, by wenzelm
removed MicroJava/BV/Convert.thy;
2001-01-07, by wenzelm
do not AutoBind.drop_judgment;
2001-01-07, by wenzelm
tuned output;
2001-01-07, by wenzelm
tuned norm_hhf(_tac);
2001-01-07, by wenzelm
added is_norm_hhf;
2001-01-07, by wenzelm
removed outdated comment;
2001-01-07, by wenzelm
case binds: AutoBind.drop_judgment;
2001-01-07, by wenzelm
tuned split_all_tac;
2001-01-07, by wenzelm
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2001-01-07, by kleing
support ?case binding;
2001-01-06, by wenzelm
apply_case: more robust handling of bounds;
2001-01-06, by wenzelm
moved norm_hhf_tac to Pure/tactic.ML;
2001-01-06, by wenzelm
added drop_judgment;
2001-01-06, by wenzelm
export read_inst', inst';
2001-01-06, by wenzelm
added list_abs;
2001-01-06, by wenzelm
added norm_hhf(_tac);
2001-01-06, by wenzelm
Tactic.norm_hhf;
2001-01-06, by wenzelm
'of:' params spec;
2001-01-06, by wenzelm
'cases' / 'induct' method: ?case binding, 'of:' spec;
2001-01-06, by wenzelm
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-05, by nipkow
^^ -> ```
2001-01-05, by nipkow
Fleuriot reference
2001-01-05, by paulson
minor edits to Chapters 1-3
2001-01-05, by paulson
revisions especially concerning the reals
2001-01-05, by paulson
*** empty log message ***
2001-01-05, by nipkow
a few extra brackets
2001-01-05, by paulson
*** empty log message ***
2001-01-05, by nipkow
*** empty log message ***
2001-01-05, by nipkow
Changed priority of dvd from 70 to 50 as befits a relation.
2001-01-05, by nipkow
*** empty log message ***
2001-01-05, by nipkow
new UNITY examples by Sidi Ehmety
2001-01-05, by paulson
Field of a relation, and some Domain/Range rules
2001-01-05, by paulson
finite_trancl: new theorem by Sidi Ehmety
2001-01-05, by paulson
more removal of obsolete rules
2001-01-05, by paulson
fixed two proofs that were affected by the removal of obsolete rules
2001-01-05, by paulson
new examples by Sidi Ehmety
2001-01-05, by paulson
tuned comment;
2001-01-04, by wenzelm
renamed .sml files to .ML;
2001-01-04, by wenzelm
label!
2001-01-04, by nipkow
more tidying, especially to remove real_of_posnat
2001-01-04, by paulson
initial material on the Reals
2001-01-04, by paulson
updated;
2001-01-03, by wenzelm
added recdef_tc(_i);
2001-01-03, by wenzelm
recdef_tc;
2001-01-03, by wenzelm
renamed .sml files to .ML;
2001-01-03, by wenzelm
TFL: renamed .sml to .ML;
2001-01-03, by wenzelm
added 'recdef_tc' command;
2001-01-03, by wenzelm
* Isar/HOL: added 'recdef_tc' command;
2001-01-03, by wenzelm
renamed .sml files to .ML;
2001-01-03, by wenzelm
tuned;
2001-01-03, by wenzelm
Thm: dest_comb, dest_abs, capply, cabs no longer global;
2001-01-03, by wenzelm
removal of the nat_cancel_factor simproc
2001-01-03, by paulson
Types chapter now uses HOL-Real
2001-01-03, by paulson
some HOL-Real material
2001-01-03, by paulson
added type annotation to Call
2001-01-02, by oheimb
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
minor tidying of simprocs
2001-01-01, by paulson
put in some missing Hyperreal files
2001-01-01, by paulson
Hyperreal
2001-01-01, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-31, by paulson
now #16*(x+y) distributes for nat just as for other numeric types
2000-12-30, by paulson
a generic ordering theorem used in Real
2000-12-30, by paulson
tidying, and separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
recover: ignore result;
2000-12-29, by wenzelm
recover: malformed result;
2000-12-29, by wenzelm
scan: malformed result;
2000-12-29, by wenzelm
recover: result;
2000-12-29, by wenzelm
proper error msg;
2000-12-29, by wenzelm
'erule' etc.: assm arg;
2000-12-27, by wenzelm
Method.erule 0;
2000-12-27, by wenzelm
updated;
2000-12-27, by wenzelm
'insert' made proper;
2000-12-27, by wenzelm
ares_tac, [edf]atac;
2000-12-27, by wenzelm
antiq: preview errors;
2000-12-23, by wenzelm
tuned length;
2000-12-23, by wenzelm
tuned output;
2000-12-23, by wenzelm
recover_order for single step tules;
2000-12-23, by wenzelm
simplified quick_and_dirty stuff;
2000-12-23, by wenzelm
tuned;
2000-12-23, by wenzelm
hide type node item;
2000-12-23, by wenzelm
Tools/string_syntax.ML;
2000-12-23, by wenzelm
tuned comment;
2000-12-23, by wenzelm
SML90 stuff;
2000-12-22, by wenzelm
handle proper rules;
2000-12-22, by wenzelm
export rewrite_cterm;
2000-12-22, by wenzelm
added inductive_conj;
2000-12-22, by wenzelm
tuned;
2000-12-22, by wenzelm
better definitions of SML90 features
2000-12-22, by paulson
*** empty log message ***
2000-12-21, by nipkow
something stopped working, had to add real_add_ac
2000-12-21, by nipkow
rational linear arithmetic
2000-12-21, by nipkow
this makes the proof run (or run faster)
2000-12-21, by paulson
further tidying of NSA proofs
2000-12-21, by paulson
*** empty log message ***
2000-12-21, by nipkow
rational arithmetic
2000-12-21, by nipkow
rational arithemtic
2000-12-21, by nipkow
re-orientation of integer literals
2000-12-21, by paulson
more tidying, especially to rationalize the simprules
2000-12-21, by paulson
re-orientation of 0=... (no idea why the backslashes have changed too)
2000-12-21, by paulson
simproc bug fix: negative literals and large terms
2000-12-21, by paulson
further tidying
2000-12-20, by paulson
generalized the re-orientation 0f 0=... to all types
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=... and 1=...
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=...
2000-12-20, by paulson
SML90: ord, chr, explode, implode;
2000-12-20, by wenzelm
re-orienting equations with #nnn on the lhs
2000-12-19, by paulson
re-orienting equations with 0, 1, 2 on the lhs
2000-12-19, by paulson
new file extract_common_term.ML for the cancel-factor simprocs
2000-12-19, by paulson
inserting the simproc nat_cancel_factor
2000-12-19, by paulson
inserting the simproc int_cancel_factor
2000-12-19, by paulson
new simprule zero_less_abs_iff
2000-12-19, by paulson
coping with the re-orientation of #nn=x
2000-12-19, by paulson
cancel-factor simproc allows shorter proofs
2000-12-19, by paulson
more tidying
2000-12-19, by paulson
cancel-factor simproc allows a shorter proof
2000-12-19, by paulson
improved errors;
2000-12-19, by wenzelm
*** empty log message ***
2000-12-18, by nipkow
*** empty log message ***
2000-12-18, by nipkow
new simproc for cancelling common factors, etc.
2000-12-18, by paulson
moved mk_bin from Numerals to HOLogic
2000-12-18, by nipkow
added rational arithmetic
2000-12-18, by nipkow
towards rtional arithmetic
2000-12-18, by nipkow
tidying and adding new proofs
2000-12-18, by paulson
loads the new simproc extract_common_term
2000-12-18, by paulson
'def': \<equiv>;
2000-12-16, by wenzelm
tuned HOL/Real/HahnBanach;
2000-12-16, by wenzelm
'def': equiv;
2000-12-16, by wenzelm
\isasymequiv;
2000-12-16, by wenzelm
updated;
2000-12-15, by wenzelm
corrected errors;
2000-12-15, by bauerg
usedir -m brackets;
2000-12-15, by wenzelm
GPLed;
2000-12-15, by wenzelm
tuned comment;
2000-12-15, by wenzelm
restore \int (integral);
2000-12-15, by wenzelm
tuned symbols;
2000-12-15, by wenzelm
further round of tidying
2000-12-15, by paulson
*** empty log message ***
2000-12-15, by nipkow
'typedef': present result theorem "type_definition Rep Abs A";
2000-12-14, by wenzelm
tuned;
2000-12-14, by wenzelm
unsymbolize;
2000-12-14, by wenzelm
use \<Sum> from main HOL;
2000-12-14, by wenzelm
added Summation;
2000-12-14, by wenzelm
many new proofs; still needs tidying
2000-12-14, by paulson
new theorem real_lbound_gt_zero
2000-12-14, by paulson
updated;
2000-12-13, by wenzelm
eliminated GOAL syntax;
2000-12-13, by wenzelm
fixed add_term_names: NameSpace.base;
2000-12-13, by wenzelm
tuned comments;
2000-12-13, by wenzelm
* print modes "brackets" and "no_brackets" control output of nested =>
2000-12-13, by wenzelm
tidying
2000-12-13, by paulson
new material, including default simprules that should be introduced earlier
2000-12-13, by paulson
fixed iter_wf proof
2000-12-13, by kleing
another round of tidying-up
2000-12-13, by paulson
working proofs up to isCont_has_Ub
2000-12-13, by paulson
tidying and replacement of "integer" rules by "order" ones
2000-12-13, by paulson
removed sorry proof
2000-12-13, by kleing
tries harder to remove negative literals, e.g.
2000-12-13, by paulson
*** empty log message ***
2000-12-13, by nipkow
*** empty log message ***
2000-12-13, by nipkow
small mods.
2000-12-13, by nipkow
sar split method uses new gen_split_tac.
2000-12-13, by nipkow
completeness (unfinished)
2000-12-12, by kleing
added direction dynamic ==> static
2000-12-12, by kleing
eliminated some warnings, tuned
2000-12-12, by kleing
first stage in tidying up Real and Hyperreal.
2000-12-12, by paulson
deleting unused rules
2000-12-12, by paulson
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
2000-12-12, by paulson
auto-updated
2000-12-12, by paulson
"translations": allow harpoons;
2000-12-11, by wenzelm
moved "_update_name" to HOL/Record;
2000-12-11, by wenzelm
tuned;
2000-12-11, by wenzelm
added "_update_name" and parse_translation;
2000-12-11, by wenzelm
alternative syntax for "translations": harpoons;
2000-12-11, by wenzelm
harpoons;
2000-12-11, by wenzelm
moved method lemma to BVSpec
2000-12-10, by kleing
kildall ==> wt_method for whole program
2000-12-10, by kleing
tuned;
2000-12-08, by wenzelm
unsymbolize;
2000-12-08, by wenzelm
tuned;
2000-12-07, by wenzelm
Id;
2000-12-07, by wenzelm
generate table of isabelle symbols;
2000-12-07, by wenzelm
removed Digest (temporarily, not up to date)
2000-12-07, by kleing
updated for is_class changes
2000-12-07, by kleing
removed two intermediate comments
2000-12-07, by oheimb
fixed and cleaned up wt[l]_jvm_prog proofs
2000-12-07, by kleing
tuned;
2000-12-07, by wenzelm
update for changes in Correct.thy and class/is_class defs
2000-12-07, by kleing
strengthened invariant: current class must be defined
2000-12-07, by kleing
update for changes in Step.thy
2000-12-07, by kleing
invoked class must be defined in Invoke C ...
2000-12-07, by kleing
unsymbolize;
2000-12-06, by wenzelm
left_minus axiom;
2000-12-06, by wenzelm
tuned;
2000-12-06, by wenzelm
activate Rational_Numbers;
2000-12-06, by wenzelm
deactivate Rational_Numbers (tmp!);
2000-12-06, by wenzelm
updated;
2000-12-06, by wenzelm
Rational_Numbers;
2000-12-06, by wenzelm
less rude treatment of "no_def";
2000-12-06, by wenzelm
added Library/Rational_Numbers.thy;
2000-12-06, by wenzelm
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
simplified interactive handling
2000-12-06, by oheimb
some derived properties;
2000-12-06, by bauerg
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
2000-12-06, by bauerg
*** empty log message ***
2000-12-06, by nipkow
converted rinv and hrinv to inverse;
2000-12-06, by bauerg
converted rinv to inverse;
2000-12-06, by bauerg
added \<a> ... \<z>;
2000-12-06, by wenzelm
tuned;
2000-12-06, by wenzelm
theory file for Numbers section
2000-12-06, by paulson
auto generated
2000-12-06, by paulson
auto update
2000-12-06, by paulson
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
2000-12-06, by paulson
miniscoping of nat_diff_split
2000-12-06, by paulson
new theory Numbers.thy
2000-12-05, by paulson
new package amsfonts
2000-12-05, by paulson
tidying
2000-12-05, by paulson
partial numerics section
2000-12-05, by paulson
nat and int sections but no real
2000-12-05, by paulson
fixed document preparation
2000-12-05, by kleing
BCV Integration
2000-12-05, by kleing
jvm_progs now also store maximum op_stack depth
2000-12-05, by kleing
*** empty log message ***
2000-12-05, by nipkow
*** empty log message ***
2000-12-04, by wenzelm
updated;
2000-12-04, by wenzelm
proper order of symbols for genarated table in system manual;
2000-12-04, by wenzelm
added \isabeginpar, \isaendpar;
2000-12-04, by wenzelm
proper order of modes;
2000-12-04, by wenzelm
diagnostic commands: comment;
2000-12-04, by wenzelm
export get_skolem;
2000-12-04, by wenzelm
fixed binding of parameters;
2000-12-04, by wenzelm
dignostic commands: comment;
2000-12-04, by wenzelm
include table of Isabelle standard symbols;
2000-12-04, by wenzelm
loads the new theory Numbers.thy
2000-12-04, by paulson
fixed formatting in section heading
2000-12-04, by paulson
auto update
2000-12-04, by paulson
tuned;
2000-12-01, by wenzelm
Now adjusted to mixed terms involving coercions.
2000-12-01, by nipkow
Linear arithmetic now copes with mixed nat/int formulae.
2000-12-01, by nipkow
append print modes;
2000-12-01, by wenzelm
no_brackets mode;
2000-12-01, by wenzelm
use_dir: modes;
2000-12-01, by wenzelm
append print_modes;
2000-12-01, by wenzelm
ignore quick_and_dirty for coind;
2000-12-01, by wenzelm
FreeUltrafilterNat ("\\<U>");
2000-12-01, by wenzelm
schematic goals;
2000-12-01, by wenzelm
removed quick_and_dirty;
2000-12-01, by wenzelm
superscripts: syntax (latex);
2000-12-01, by wenzelm
usedir: -m option;
2000-12-01, by wenzelm
added \mathcal A-Z;
2000-12-01, by wenzelm
option -m;
2000-12-01, by wenzelm
*** empty log message ***
2000-12-01, by nipkow
*** empty log message ***
2000-12-01, by nipkow
many new div and mod properties (borrowed from Integ/IntDiv)
2000-12-01, by paulson
renamed less_eq_Suc_add to less_imp_Suc_add
2000-12-01, by paulson
tuned;
2000-11-30, by wenzelm
removed "./configure";
2000-11-30, by wenzelm
/usr/bin/env bash;
2000-11-30, by wenzelm
schematic props;
2000-11-30, by wenzelm
removed get_goal;
2000-11-30, by wenzelm
added is_replaced_dummy_pattern;
2000-11-30, by wenzelm
renamed "equivalence_class" to "class";
2000-11-30, by wenzelm
schematic goals;
2000-11-30, by wenzelm
cases/induct: tuned handling of facts ('consumes');
2000-11-30, by wenzelm
'consumes' att;
2000-11-30, by wenzelm
misc;
2000-11-30, by wenzelm
replaced Eps by SOME
2000-11-30, by paulson
*** empty log message ***
2000-11-30, by nipkow
some properties;
2000-11-30, by bauerg
*** empty log message ***
2000-11-30, by nipkow
resolveq_cases_tac moved here from Pure/Isar/method.ML;
2000-11-29, by wenzelm
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
2000-11-29, by wenzelm
expand_split_asm -> split_split_asm
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
simproc for cancelling common factors around = < <= div /
2000-11-29, by paulson
invoking CancelNumeralFactorFun
2000-11-29, by paulson
new simproc file cancel_numeral_factor.ML
2000-11-29, by paulson
added a reference to {sec:products} for ordered pair reasoning
2000-11-28, by paulson
fixed hostname;
2000-11-28, by wenzelm
detect CVSROOT;
2000-11-28, by wenzelm
tuned;
2000-11-28, by wenzelm
added consumes, consumes_default;
2000-11-28, by wenzelm
resolveq_cases_tac: insert facts;
2000-11-28, by wenzelm
added "consumes" attribute;
2000-11-28, by wenzelm
consume facts;
2000-11-28, by wenzelm
consumes0/1;
2000-11-28, by wenzelm
RuleCases.save;
2000-11-28, by wenzelm
*** empty log message ***
2000-11-27, by nipkow
deleted unused result intrel_refl
2000-11-27, by paulson
*** empty log message ***
2000-11-27, by nipkow
*** empty log message ***
2000-11-26, by nipkow
*** empty log message ***
2000-11-26, by nipkow
hide many names from Datatype_Universe.
2000-11-24, by nipkow
exception Interrupt = SML90.Interrupt;
2000-11-24, by wenzelm
added exception Interrupt for use in function Library/try
2000-11-24, by paulson
arith_tac: atomize;
2000-11-23, by wenzelm
standard: close_derivation;
2000-11-23, by wenzelm
* HOL: syntax or "abs";
2000-11-23, by wenzelm
*** empty log message ***
2000-11-23, by nipkow
tuned;
2000-11-22, by wenzelm
tuned;
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by nipkow
tag result with name reference to final binding (basically just a comment);
2000-11-21, by wenzelm
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-21, by wenzelm
replace \<dots>;
2000-11-21, by wenzelm
unsymbolize;
2000-11-21, by wenzelm
quote executable;
2000-11-21, by wenzelm
tuned;
2000-11-21, by wenzelm
;
2000-11-21, by bauerg
adjusted for BV changes (Ok -> OK)
2000-11-21, by kleing
thebibliography environment: replaced the Springer version by the standard one
2000-11-21, by paulson
alternative function definition;
2000-11-21, by bauerg
*** empty log message ***
2000-11-21, by nipkow
BCV integration (type system is semilattice)
2000-11-20, by kleing
BCV integration (first step)
2000-11-20, by kleing
export freeze_thaw_type;
2000-11-18, by wenzelm
improved messages;
2000-11-18, by wenzelm
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18, by wenzelm
axclass ordered_ring;
2000-11-18, by wenzelm
quot_cond_function: simplified, support conditional definition;
2000-11-18, by wenzelm
abs_eq_0: #0 instead of 0;
2000-11-18, by wenzelm
symbol syntax for "abs";
2000-11-18, by wenzelm
added axclass ordered_field;
2000-11-18, by wenzelm
check result: Envir.beta_norm;
2000-11-17, by wenzelm
Envir.beta_norm;
2000-11-17, by wenzelm
added beta_norm;
2000-11-17, by wenzelm
tuned;
2000-11-17, by wenzelm
removed quot_cond_function1, quot_function1;
2000-11-17, by wenzelm
UNIV_witness;
2000-11-17, by wenzelm
Ring_and_Field;
2000-11-17, by wenzelm
Library/Ring_and_Field.thy;
2000-11-17, by wenzelm
rings and fields;
2000-11-16, by bauerg
Proof.assert_forward;
2000-11-16, by wenzelm
added not_equiv_sym, not_equiv_trans1/2;
2000-11-16, by wenzelm
added abs_mult, abs_eq_0, square_nonzero;
2000-11-16, by wenzelm
ground terms section: new intro
2000-11-16, by paulson
CTT
2000-11-16, by paulson
separate rules for function/operation definitions;
2000-11-15, by wenzelm
renamed integ_le_less to int_le_less;
2000-11-15, by wenzelm
updated;
2000-11-15, by wenzelm
isabellebody: \par at begin/end;
2000-11-15, by wenzelm
auto update
2000-11-14, by paulson
first version of Advanced Inductive Defs section
2000-11-14, by paulson
x-symbol support for Pi, Sigma, -->, : (membership)
2000-11-14, by paulson
new Main.thy as in HOL, ZF
2000-11-14, by paulson
added read_terms, read_props (simulataneous type-inference);
2000-11-13, by wenzelm
tuned statement args;
2000-11-13, by wenzelm
tuned IsarThy.theorem_i;
2000-11-13, by wenzelm
added students
2000-11-13, by kleing
Removed > and >=
2000-11-13, by nipkow
Removed > and >= again.
2000-11-13, by nipkow
quot_cond_definition;
2000-11-12, by wenzelm
simplified induction;
2000-11-12, by wenzelm
updated;
2000-11-12, by wenzelm
"induct" method: handle proper rules;
2000-11-12, by wenzelm
removed warning for "stripped" option;
2000-11-12, by wenzelm
removed junk;
2000-11-12, by wenzelm
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-11-12, by wenzelm
* added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10, by wenzelm
int_distrib;
2000-11-10, by wenzelm
nat_distrib;
2000-11-10, by wenzelm
hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
2000-11-10, by wenzelm
tuned;
2000-11-10, by wenzelm
use inverse, divide from basic HOL;
2000-11-10, by wenzelm
norm_hhf_tac;
2000-11-10, by wenzelm
rewrite_goal_tac moved to tactic.ML;
2000-11-10, by wenzelm
added rewrite_goal_tac;
2000-11-10, by wenzelm
added certify_tycon, certify_tyabbr, certify_const;
2000-11-10, by wenzelm
has_meta_prems: include "==";
2000-11-10, by wenzelm
store_standard_thm "norm_hhf_eq";
2000-11-10, by wenzelm
proper theory context for mesontest2;
2000-11-10, by wenzelm
inductive_rulify2 accomodates malformed induction rules;
2000-11-10, by wenzelm
Sign.certify_tycon, Sign.certify_const;
2000-11-10, by wenzelm
improved cong_definition theorems;
2000-11-10, by wenzelm
simplified induction;
2000-11-10, by wenzelm
added axclass power (from HOL.thy);
2000-11-10, by wenzelm
simplified atomize;
2000-11-10, by wenzelm
axclass power moved to Nat.thy;
2000-11-10, by wenzelm
added axclass inverse and consts inverse, divide (infix "/");
2000-11-10, by wenzelm
FOL_basic_ss: simprocs moved to FOL_ss;
2000-11-10, by wenzelm
added atomize_eq;
2000-11-10, by wenzelm
val atomize = thms "atomize'";
2000-11-10, by wenzelm
> etc
2000-11-10, by nipkow
new: > and >=
2000-11-10, by nipkow
rule inversion
2000-11-10, by nipkow
JMB -> JMPB. Email von Johannes Pfeifroth.
2000-11-10, by nipkow
updated;
2000-11-09, by wenzelm
fixed \title: convert "_" to "-";
2000-11-09, by wenzelm
tuned isabelle environment;
2000-11-08, by wenzelm
subgoals
2000-11-08, by nipkow
*** empty log message ***
2000-11-08, by nipkow
better discussion of rule induction
2000-11-07, by paulson
Thm.dest_abs now takes an additional argument.
2000-11-07, by berghofe
Moved rewriting functions from Thm to MetaSimplifier.
2000-11-07, by berghofe
- Moved rewriting functions to meta_simplifier.ML
2000-11-07, by berghofe
moved rewriting functions from Drule to MetaSimplifier
2000-11-07, by berghofe
- new theorems imp_cong and swap_prems_eq
2000-11-07, by berghofe
Added new file meta_simplifier.ML
2000-11-07, by berghofe
Moved meta simplification stuff from Thm to MetaSimplifier.
2000-11-07, by berghofe
Added type constraint in theorem "lift".
2000-11-07, by berghofe
*** empty log message ***
2000-11-07, by nipkow
method 'induct' now handles non-atomic goals;
2000-11-06, by wenzelm
improved: 'induct' handle non-atomic goals;
2000-11-06, by wenzelm
make: open_parms argument;
2000-11-06, by wenzelm
RuleCases.make true;
2000-11-06, by wenzelm
added rewrite_goal_tac;
2000-11-06, by wenzelm
added typ_instance;
2000-11-06, by wenzelm
Sign.typ_instance;
2000-11-06, by wenzelm
inductive_atomize, inductive_rulify;
2000-11-06, by wenzelm
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
2000-11-06, by wenzelm
tuned atomize_goal;
2000-11-06, by wenzelm
minor modifications for new Springer style
2000-11-06, by paulson
minor changes
2000-11-06, by paulson
auto update
2000-11-06, by paulson
*** empty log message ***
2000-11-06, by nipkow
updated;
2000-11-04, by wenzelm
tuned method "rule" and "default";
2000-11-04, by wenzelm
isamarkup: handle % in input;
2000-11-04, by wenzelm
tuned;
2000-11-04, by wenzelm
misc stuff;
2000-11-04, by wenzelm
tuned;
2000-11-03, by wenzelm
proper setup of "parallel";
2000-11-03, by wenzelm
tuned notation;
2000-11-03, by wenzelm
adapted "obtain" proofs;
2000-11-03, by wenzelm
provide case names for rev_induct, rev_cases;
2000-11-03, by wenzelm
rev_exhaust: rulify;
2000-11-03, by wenzelm
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03, by wenzelm
"atomize" for classical tactics;
2000-11-03, by wenzelm
atomize: all automated tactics that "solve" goals;
2000-11-03, by wenzelm
fixed two obscurities of "fix": predeclare_terms;
2000-11-03, by wenzelm
tuned names;
2000-11-03, by wenzelm
improved handling of "that": insert into goal, only declare as Pure "intro";
2000-11-03, by wenzelm
assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03, by wenzelm
added atomic_judgment;
2000-11-03, by wenzelm
structure Obtain = Obtain;
2000-11-03, by wenzelm
new lemma card_Diff2_less for mulilated chess board
2000-11-03, by paulson
*** empty log message ***
2000-11-03, by nipkow
*** empty log message ***
2000-11-03, by nipkow
*** empty log message ***
2000-11-03, by nipkow
the section command will belong to the new file
2000-11-03, by paulson
advanced induction examples
2000-11-03, by paulson
auto update?
2000-11-03, by paulson
replaced Acc.thy by Advanced.thy
2000-11-03, by paulson
no longer needed: too complicated an example
2000-11-02, by paulson
*** empty log message ***
2000-11-02, by nipkow
auto generated
2000-11-02, by paulson
tuned goal output;
2000-10-31, by wenzelm
*** empty log message ***
2000-10-31, by nipkow
*** empty log message ***
2000-10-31, by nipkow
updated;
2000-10-30, by wenzelm
tuned goals output;
2000-10-30, by wenzelm
improved statement bindings for props;
2000-10-30, by wenzelm
converse: syntax \<inverse>;
2000-10-30, by wenzelm
tuned;
2000-10-30, by wenzelm
added ex/PER.thy;
2000-10-30, by wenzelm
improved doc of "subgoals" antiquotation;
2000-10-30, by wenzelm
replaced \isasymmacron by \isasyminverse;
2000-10-30, by wenzelm
tuned tex template;
2000-10-30, by wenzelm
Partial equivalence relations (leftover from HOL/Quot);
2000-10-30, by wenzelm
added antiq. subgoals
2000-10-30, by nipkow
Added antiquotation "subgoals".
2000-10-30, by nipkow
Mod because of additional parameters to pretty_goals.
2000-10-30, by nipkow
back to 1.167, due to Emacs/CVS casualty!!;
2000-10-27, by wenzelm
added instantiate_tac
2000-10-27, by oheimb
*** empty log message ***
2000-10-27, by wenzelm
removed isabelle resources: are available from main pages
2000-10-27, by kleing
cleanup, looks ok now with konqueror, too
2000-10-27, by kleing
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
added the $Id:$ line
2000-10-26, by paulson
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
use Library/List_Prefix;
2000-10-25, by wenzelm
added HOL/Library/List_Prefix;
2000-10-25, by wenzelm
improved antiquotations;
2000-10-25, by wenzelm
added \isarantiq;
2000-10-25, by wenzelm
add \<le> to list of "good" symbols;
2000-10-25, by wenzelm
tuned names;
2000-10-25, by wenzelm
added List_Prefix;
2000-10-25, by wenzelm
more "xsymbols" syntax;
2000-10-25, by wenzelm
"List prefixes" library theory (replaces old Lex/Prefix);
2000-10-25, by wenzelm
*** empty log message ***
2000-10-25, by nipkow
*** empty log message ***
2000-10-25, by nipkow
inputs Even.tex
2000-10-25, by paulson
minor tinkering
2000-10-25, by paulson
Even numbers section of Inductive chapter
2000-10-25, by paulson
tuned msg;
2000-10-25, by wenzelm
antiquotation "goals": error message;
2000-10-25, by wenzelm
* support sub/super scripts (for single symbols only), input syntax is
2000-10-24, by wenzelm
let commands access Toplevel.state;
2000-10-24, by wenzelm
added pretty_goals;
2000-10-24, by wenzelm
added antiquotation "goals" and option "goals_limit";
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
added clasimpset: unit -> clasimpset;
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
Acc example
2000-10-24, by paulson
even numbers example
2000-10-24, by paulson
intro_classes by default;
2000-10-23, by wenzelm
declare trancl rules;
2000-10-23, by wenzelm
tuned;
2000-10-23, by wenzelm
updated;
2000-10-23, by wenzelm
intro_classes by default;
2000-10-23, by wenzelm
make sure default document works;
2000-10-23, by wenzelm
comment out Pure-copied target;
2000-10-23, by wenzelm
* HOL: default proof step now includes 'intro_classes';
2000-10-23, by wenzelm
*** empty log message ***
2000-10-23, by nipkow
part of set-up
2000-10-23, by paulson
sets chapter
2000-10-23, by paulson
fixed crossref
2000-10-23, by paulson
tidied
2000-10-23, by paulson
X-symbol
2000-10-23, by paulson
auto gen
2000-10-23, by paulson
addition of Rules, Sets and some macros of lcp
2000-10-23, by paulson
goodbye to this dummy file
2000-10-23, by paulson
now includes Rules, Sets (?)
2000-10-23, by paulson
the Rules chapter and theories
2000-10-23, by paulson
the Sets chapter and theories
2000-10-23, by paulson
quantifiers now allowed in inductive defs
2000-10-23, by paulson
tidied
2000-10-23, by paulson
isatool unsymbolize;
2000-10-23, by wenzelm
added type_definitionI;
2000-10-23, by wenzelm
tuned deps;
2000-10-23, by wenzelm
contrapos
2000-10-23, by paulson
two spelling fixes
2000-10-23, by paulson
tuned;
2000-10-22, by wenzelm
simplified quotients (only plain total equivs);
2000-10-22, by wenzelm
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
provide more theorems (see subset.thy);
2000-10-19, by wenzelm
InductAttrib;
2000-10-19, by wenzelm
improved typedef;
2000-10-19, by wenzelm
improved typedef;
2000-10-19, by wenzelm
added theory for HOL type definitions;
2000-10-19, by wenzelm
tuned;
2000-10-19, by wenzelm
added Tools/induct_attrib.ML;
2000-10-19, by wenzelm
declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-19, by wenzelm
tuned \isasymuniqex;
2000-10-19, by wenzelm
split over two files: induct_attrib.ML, induct_method.ML;
2000-10-19, by wenzelm
tuned;
2000-10-19, by wenzelm
use RecdefPackage.tcs_of;
2000-10-19, by wenzelm
added tcs_of;
2000-10-19, by wenzelm
updated;
2000-10-18, by wenzelm
removed Library/Accessible_Part.ML;
2000-10-18, by wenzelm
use Multiset from HOL/Library;
2000-10-18, by wenzelm
use Accessible_Part from HOL/Library;
2000-10-18, by wenzelm
path_add "~~/src/HOL/Library";
2000-10-18, by wenzelm
tuned;
2000-10-18, by wenzelm
tuned declarations;
2000-10-18, by wenzelm
avoid "_" and "^" (more robust);
2000-10-18, by wenzelm
removed Acc and Multiset (see HOL/Library);
2000-10-18, by wenzelm
moved to HOL/Library;
2000-10-18, by wenzelm
MultisetOrder mmoved to HOL/Library;
2000-10-18, by wenzelm
moved to HOL/LIbrary;
2000-10-18, by wenzelm
added HOL/Library, rearranged several files;
2000-10-18, by wenzelm
moved to HOL/Library;
2000-10-18, by wenzelm
"The Supplemental Isabelle/HOL Library";
2000-10-18, by wenzelm
added path_add;
2000-10-18, by wenzelm
A general ``while'' combinator (from main HOL);
2000-10-18, by wenzelm
Quotient types;
2000-10-18, by wenzelm
Multisets (from HOL/Induct/Multiset and friends);
2000-10-18, by wenzelm
The accessible part of a relation (from HOL/Induct/Acc);
2000-10-18, by wenzelm
\isabellecontext: output_syms;
2000-10-18, by wenzelm
restart: do not reset theory loader path;
2000-10-18, by wenzelm
* HOL/Library: a collection of generic theories to be used together
2000-10-18, by wenzelm
*** empty log message ***
2000-10-18, by nipkow
*** empty log message ***
2000-10-18, by nipkow
*** empty log message ***
2000-10-18, by nipkow
wellfounded -> well-founded
2000-10-18, by paulson
tuned;
2000-10-17, by wenzelm
"Deriving rules";
2000-10-17, by wenzelm
improved;
2000-10-17, by wenzelm
*** empty log message ***
2000-10-17, by nipkow
*** empty log message ***
2000-10-17, by nipkow
renaming of contrapos rules
2000-10-17, by paulson
tidied some awkward proofs
2000-10-17, by paulson
tidying; removed unused rev_contra_subsetD
2000-10-17, by paulson
restoration of "equalityI"; renaming of contrapos rules
2000-10-17, by paulson
renaming of contrapos rules
2000-10-17, by paulson
tidying and renaming of contrapos rules
2000-10-17, by paulson
cosmetics
2000-10-17, by oheimb
added intermediate value thms
2000-10-17, by nipkow
<= -> \<le>
2000-10-17, by nipkow
updated;
2000-10-16, by wenzelm
*** empty log message ***
2000-10-16, by nipkow
*** empty log message ***
2000-10-16, by nipkow
tuned;
2000-10-15, by wenzelm
fixed \isasyminv;
2000-10-15, by wenzelm
more elements;
2000-10-15, by wenzelm
proper symbol markup with \isamath, \isatext;
2000-10-15, by wenzelm
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
renamed fp_Tarski to fp_unfold
2000-10-13, by paulson
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-12, by nipkow
*** empty log message ***
2000-10-12, by nipkow
updated;
2000-10-12, by wenzelm
induct -> lfp_induct;
2000-10-12, by wenzelm
install default_handler for SIGINT initially as well;
2000-10-12, by wenzelm
tuned syms;
2000-10-12, by wenzelm
updated;
2000-10-12, by wenzelm
accomodate Poly/ML 4.0;
2000-10-12, by wenzelm
even smarter setup for several installations of Poly/ML 3.x and 4.0;
2000-10-12, by wenzelm
tuned syms;
2000-10-12, by wenzelm
removed nonsensical print statement;
2000-10-12, by wenzelm
induct -> lfp_induct
2000-10-12, by nipkow
tidied
2000-10-12, by paulson
new theorem and SD-rule zmod_eq_0_iff
2000-10-12, by paulson
delrules [r_into_rtrancl] required because the new I-rule made a step slow.
2000-10-12, by paulson
tidied
2000-10-12, by paulson
renamed ?Pa to ?Q in swap
2000-10-12, by paulson
new I-rules r_into_rtrancl, r_into_trancl and a simpler proof
2000-10-12, by paulson
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
2000-10-12, by paulson
improved exhibit_interrupt;
2000-10-12, by wenzelm
\isamath and \isatext: more abstract implementation of symbols;
2000-10-11, by wenzelm
*** empty log message ***
2000-10-11, by nipkow
*** empty log message ***
2000-10-11, by nipkow
*** empty log message ***
2000-10-11, by nipkow
*** empty log message ***
2000-10-11, by nipkow
fixed \isastyleminor for "tt": \small;
2000-10-11, by wenzelm
*** empty log message ***
2000-10-11, by nipkow
*** empty log message ***
2000-10-11, by nipkow
fixed 'clarify': CHANGED;
2000-10-11, by wenzelm
fully enclose "\isadigit{...}";
2000-10-10, by wenzelm
tuned;
2000-10-10, by wenzelm
AddXEs [someI_ex];
2000-10-10, by wenzelm
added a section label
2000-10-10, by paulson
fixed hrefs: index.html;
2000-10-09, by wenzelm
added rtranclIs
2000-10-09, by nipkow
*** empty log message ***
2000-10-09, by nipkow
*** empty log message ***
2000-10-09, by nipkow
tuned text;
2000-10-09, by wenzelm
ex_someI -> someI_ex
2000-10-09, by nipkow
simplified rtrancl_converse{I,D}
2000-10-09, by paulson
got rid of a swap
2000-10-09, by paulson
expandshort
2000-10-09, by paulson
*** empty log message ***
2000-10-09, by nipkow
@ -> SOME
2000-10-09, by nipkow
tuned;
2000-10-08, by wenzelm
final tuning;
Isabelle99-1
2000-10-06, by wenzelm
tuned;
2000-10-06, by wenzelm
tuned;
2000-10-06, by wenzelm
tuned;
2000-10-06, by wenzelm
* HOL/IMPP: extension of IMP with local variables and mutually
2000-10-06, by wenzelm
updated, improved;
2000-10-06, by wenzelm
tuned;
2000-10-06, by wenzelm
draft for 99-1;
2000-10-06, by wenzelm
tuned;
2000-10-06, by wenzelm
*** empty log message ***
2000-10-06, by nipkow
tuned;
2000-10-06, by wenzelm
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
2000-10-06, by wenzelm
Updated README file for HOL/Real
2000-10-05, by fleuriot
new 'THEN' syntax;
2000-10-04, by wenzelm
tuned;
2000-10-04, by wenzelm
added more stuff;
2000-10-04, by wenzelm
improved @;
2000-10-04, by wenzelm
'THEN', 'COMP': improved optional position arg;
2000-10-04, by wenzelm
added "bracks";
2000-10-04, by wenzelm
*** empty log message ***
2000-10-04, by nipkow
Hoare logic in Isar;
2000-10-03, by wenzelm
tuned deps;
2000-10-03, by wenzelm
tuned;
2000-10-03, by wenzelm
added Hoare;
2000-10-03, by wenzelm
hide declaratations;
2000-10-03, by wenzelm
added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
2000-10-03, by wenzelm
unsymbolized;
2000-10-03, by wenzelm
tuned names;
2000-10-03, by wenzelm
major cleanup -- improved typesetting;
2000-10-03, by wenzelm
unsymbolize;
2000-10-03, by wenzelm
eliminated \<oplus>;
2000-10-03, by wenzelm
removed "symbols" syntax for constant "override";
2000-10-03, by wenzelm
reorganized AxClasses;
2000-10-03, by wenzelm
reorganized AxClasses;
2000-10-03, by wenzelm
moved axclass tutorial examples to top dir;
2000-10-03, by wenzelm
*** empty log message ***
2000-10-03, by nipkow
updated;
2000-10-03, by wenzelm
range declared as syntax;
2000-10-03, by wenzelm
added == transitive rule (bad idea??);
2000-10-02, by wenzelm
improved t.weak_case_cong text;
2000-10-02, by wenzelm
delcongs weak_case_congs;
2000-10-02, by wenzelm
renamed "None" to "NONE" (avoid clash with option type);
2000-10-02, by wenzelm
qed "";
2000-10-02, by wenzelm
tuned;
2000-10-02, by wenzelm
*** empty log message ***
2000-10-02, by nipkow
*** empty log message ***
2000-10-02, by nipkow
*** empty log message ***
2000-10-02, by nipkow
export get_datatypes_sg;
2000-10-02, by wenzelm
info: weak_case_cong;
2000-10-02, by wenzelm
separated expr and stmt
2000-10-02, by nipkow
isapar: \medskip;
2000-09-30, by wenzelm
Now some functions try to avoid name clashes when introducing new free
2000-09-29, by berghofe
tuned;
2000-09-29, by wenzelm
tuned;
2000-09-29, by wenzelm
tuned;
2000-09-28, by wenzelm
include log files;
2000-09-28, by wenzelm
tuned;
2000-09-28, by wenzelm
some preliminary stuff on conversion;
2000-09-28, by wenzelm
fixed ref;
2000-09-28, by wenzelm
record proof tools: t.equality;
2000-09-28, by wenzelm
isabelle -C;
2000-09-28, by wenzelm
www.proofgeneral.org;
2000-09-28, by wenzelm
fixed \<Union>, \<Inter> syntax;
2000-09-28, by wenzelm
added COPYDB argument;
2000-09-28, by wenzelm
option -C;
2000-09-28, by wenzelm
Isabelle99-1 (October 2000);
2000-09-28, by wenzelm
support copy option;
2000-09-28, by wenzelm
./build -b -m Pure-copied Pure;
2000-09-28, by wenzelm
only run quick_and_dirty version by default;
2000-09-28, by wenzelm
tuned;
2000-09-28, by wenzelm
deleted card_0_empty_iff because it is the same as card_0_eq;
2000-09-28, by paulson
THIS_IS_ISABELLE_BUILD;
2000-09-27, by wenzelm
tuned;
2000-09-27, by wenzelm
tuned comment;
2000-09-27, by wenzelm
proper Hyperreal setup;
2000-09-27, by wenzelm
more symbolic syntax (currently "input");
2000-09-27, by wenzelm
exchanged the declaration of "seealso" and loading of "makeidx" because the
2000-09-27, by paulson
tuned;
2000-09-26, by wenzelm
FAKE_BUILD="";
2000-09-26, by wenzelm
updated;
2000-09-26, by wenzelm
updated;
2000-09-26, by wenzelm
tuned;
2000-09-26, by wenzelm
replaced by document (cannot maintain both);
2000-09-26, by wenzelm
simplified;
2000-09-26, by wenzelm
weblint;
2000-09-26, by wenzelm
got rid of RPM;
2000-09-26, by wenzelm
make Isabelle logic images for current platform;
2000-09-26, by wenzelm
simplified;
2000-09-26, by wenzelm
HOL/MicroJava;
2000-09-26, by wenzelm
www.proofgeneral.org;
2000-09-26, by wenzelm
updated url;
2000-09-26, by wenzelm
tuned;
2000-09-26, by wenzelm
removed the obsolete (and badly named) inj_select
2000-09-26, by paulson
tuned;
2000-09-25, by wenzelm
tuned;
2000-09-25, by wenzelm
tuned;
2000-09-25, by wenzelm
tuned;
2000-09-25, by wenzelm
tuned replacements;
2000-09-25, by wenzelm
tuned auto paths;
2000-09-25, by wenzelm
untabified for HTML
2000-09-25, by kleing
include "Isabelle" link;
2000-09-25, by wenzelm
tidied, removing obsolete "goal" commands
2000-09-23, by paulson
new theorems and comment
2000-09-23, by paulson
renaming the inverse image operator in HOL
2000-09-23, by paulson
added compatibility relation: AllowedActs, Allowed, ok,
2000-09-23, by paulson
tuned comments;
2000-09-22, by wenzelm
AddXIs [equal_intr_rule];
2000-09-22, by wenzelm
added HTML syntax; added spaces in normal syntax for better documents
2000-09-22, by kleing
added HTML syntax
2000-09-22, by kleing
removed JVM/Store.ML, added theorem Digest in MicroJava
2000-09-22, by kleing
lemma now in Store.thy
2000-09-22, by kleing
converted to Isar, tuned
2000-09-22, by kleing
tuned spacing for document generation
2000-09-21, by kleing
*** empty log message ***
2000-09-21, by fleuriot
renamed to Records.thy;
2000-09-21, by wenzelm
improved \isachartilde for non-tt styles;
2000-09-21, by wenzelm
renamed HOL/ex/Points to HOL/ex/Records;
2000-09-21, by wenzelm
added height="100%" to stretch page to whole browser window
2000-09-21, by kleing
added headline, "quick download", and mailing list archive
2000-09-21, by kleing
added height="100%" to stretch page to whole browser window
2000-09-21, by kleing
*** empty log message ***
2000-09-21, by wenzelm
Digest.thy as toplevel theory
2000-09-21, by kleing
theorem digest of all MicroJava theorems, theories in alphabetical order
2000-09-21, by kleing
New theories: construction of hypernaturals, nonstandard extensions,
2000-09-21, by fleuriot
tuned, added lightweight BV to abstract, added Bali link
2000-09-21, by kleing
Updated Files with new theorems
2000-09-21, by fleuriot
unsymbolized
2000-09-21, by kleing
removed dead code;
2000-09-20, by wenzelm
added "install" target;
2000-09-20, by wenzelm
tuned;
2000-09-20, by wenzelm
tuned rpm command lines;
2000-09-20, by wenzelm
updated;
2000-09-20, by wenzelm
made SML/NJ happy;
2000-09-20, by wenzelm
added common args keywords;
2000-09-19, by wenzelm
tuned args;
2000-09-19, by wenzelm
added iff_add_global', iff_add_local' (syntax "iff?");
2000-09-19, by wenzelm
tuned;
2000-09-19, by wenzelm
attribute / modifier 'iff': support "?" mode;
2000-09-19, by wenzelm
tuned msg;
2000-09-19, by wenzelm
updated;
2000-09-19, by wenzelm
tuned;
2000-09-18, by wenzelm
tuned;
2000-09-18, by wenzelm
remove unreadable symbol names from sources;
2000-09-18, by wenzelm
tuned;
2000-09-18, by wenzelm
added plain "tt" style;
2000-09-18, by wenzelm
*** empty log message ***
2000-09-18, by wenzelm
rpm --force;
2000-09-18, by wenzelm
best-style made default;
2000-09-18, by wenzelm
tuned;
2000-09-18, by wenzelm
tuned;
2000-09-18, by wenzelm
tuned;
2000-09-18, by wenzelm
include ANNOUNCE;
2000-09-18, by wenzelm
improved pages;
2000-09-18, by wenzelm
indicate occurrences of 'handle _';
2000-09-18, by wenzelm
removed -x option;
2000-09-17, by wenzelm
made SML/NJ happy;
2000-09-17, by wenzelm
less
more
|
(0)
-10000
-1536
+1536
+10000
+30000
tip