Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3072
+3072
+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
AddXIs [prod_eqI];
2000-09-17, by wenzelm
AddXIs [ext];
2000-09-17, by wenzelm
added print_thm(s)_sg;
2000-09-17, by wenzelm
begin_theory: removed message;
2000-09-17, by wenzelm
Display.pretty_thm_sg;
2000-09-17, by wenzelm
isar-strip-terminators;
2000-09-17, by wenzelm
tuned;
2000-09-17, by wenzelm
updated;
2000-09-17, by wenzelm
safe_asm_full_simp_tac is back (for compat);
2000-09-15, by wenzelm
cleaned up and prepared for Isabelle99-1;
2000-09-15, by wenzelm
*** empty log message ***
2000-09-15, by wenzelm
added;
2000-09-15, by wenzelm
someI2_ex;
2000-09-15, by wenzelm
added "congs" keyword;
2000-09-15, by wenzelm
fixed someI2_ex;
2000-09-15, by wenzelm
keep export of ISABELLE_TMP (!!!);
2000-09-15, by wenzelm
added s/selectI/someI/g;
2000-09-15, by wenzelm
tuned;
2000-09-15, by wenzelm
XSYMBOL_INSTALLFONTS is back;
2000-09-15, by wenzelm
*** empty log message ***
2000-09-15, by nipkow
*** empty log message ***
2000-09-15, by nipkow
"hints" made keyword again;
2000-09-15, by wenzelm
hunting gremlins ...;
2000-09-15, by wenzelm
tentative fix while hunting gremlins ...;
2000-09-15, by wenzelm
added new papers
2000-09-15, by oheimb
added mJava macro
2000-09-15, by oheimb
added new papers
2000-09-15, by oheimb
added mJava macro
2000-09-15, by oheimb
isatool installfonts: -x option;
2000-09-15, by wenzelm
isabelle: -P option;
2000-09-15, by wenzelm
tuned msg;
2000-09-15, by wenzelm
system: isatool installfonts may handle X-Symbol fonts as well;
2000-09-15, by wenzelm
added latexsym (no longer loaded by isabellesym);
2000-09-15, by wenzelm
tuned init sequence;
2000-09-15, by wenzelm
ML_command: no_timing;
2000-09-15, by wenzelm
unexport exports;
2000-09-15, by wenzelm
added lparr, rparr;
2000-09-15, by wenzelm
fixed "sl" style;
2000-09-15, by wenzelm
support XSYMBOL_INSTALLFONTS as well;
2000-09-15, by wenzelm
#XSYMBOL_INSTALLFONTS;
2000-09-15, by wenzelm
-P option;
2000-09-15, by wenzelm
renamed the select rules
2000-09-15, by paulson
the final renaming: selectI -> someI
2000-09-15, by paulson
renamed (most of...) the select rules
2000-09-15, by paulson
fixed comment;
2000-09-15, by wenzelm
fixed name;
2000-09-15, by wenzelm
fix theorem names related to SOME (Eps) in HOL;
2000-09-15, by wenzelm
tuned spacing of symbols syntax;
2000-09-15, by wenzelm
tuned symbols;
2000-09-15, by wenzelm
handle more symbols;
2000-09-15, by wenzelm
improved many symbols;
2000-09-15, by wenzelm
updated;
2000-09-15, by wenzelm
renamed "bow" to "frown";
2000-09-15, by wenzelm
"Isabelle repository version";
2000-09-14, by wenzelm
*** empty log message ***
2000-09-14, by nipkow
*** empty log message ***
2000-09-14, by nipkow
added /usr/share/emacs/ProofGeneral/isar/interface choice;
2000-09-14, by wenzelm
a bit more of division
2000-09-14, by paulson
dummy (generated by makedist);
2000-09-13, by wenzelm
begin_theory: priority message to gain some robustness in sync communication;
2000-09-13, by wenzelm
Args.addN, Args.delN;
2000-09-13, by wenzelm
LFilter: setmp quick_and_dirty false;
2000-09-13, by wenzelm
\<epsilon>: syntax (input);
2000-09-13, by wenzelm
tuned recdef hints;
2000-09-13, by wenzelm
easy settings: add /usr/local prefix;
2000-09-13, by wenzelm
updated to 3.3d;
2000-09-13, by wenzelm
tar packages: /usr/local;
2000-09-13, by wenzelm
more integer theorems, better simplification
2000-09-13, by paulson
moved Primes, Fib, Factorization from HOL/ex
2000-09-13, by paulson
zgcd now works for negative integers
2000-09-13, by paulson
moved Primes, Fib, Factorization to HOL/NumberTheory
2000-09-13, by paulson
renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12, by wenzelm
*** empty log message ***
2000-09-12, by nipkow
tuned handling of "intros";
2000-09-12, by wenzelm
delrule: handle dest rules as well;
2000-09-12, by wenzelm
replaced "delrule" by "rule del";
2000-09-12, by wenzelm
renamed "delrule" to "rule del";
2000-09-12, by wenzelm
tuned;
2000-09-12, by wenzelm
tuned;
2000-09-12, by wenzelm
*** empty log message ***
2000-09-12, by nipkow
*** empty log message ***
2000-09-12, by nipkow
added MicroJava/document/root.bib;
2000-09-12, by wenzelm
tidying and updating for revised Mutilated Chess Board article
2000-09-12, by paulson
simple RPM spec for in-situ package;
2000-09-11, by wenzelm
template;
2000-09-11, by wenzelm
tuned;
2000-09-11, by wenzelm
simple RPM spec for in-situ package;
2000-09-11, by wenzelm
tuned;
2000-09-11, by wenzelm
updated;
2000-09-11, by wenzelm
renamed "rulify" to "rulified";
2000-09-11, by wenzelm
dummy;
2000-09-11, by wenzelm
updated;
2000-09-11, by wenzelm
improved WWW page generation (still somewhat experimental);
2000-09-11, by wenzelm
added title, abstract, bibliography;
2000-09-11, by wenzelm
proper markup of schematic (!) skolems;
2000-09-11, by wenzelm
support \isabellecontext;
2000-09-11, by wenzelm
define \isabellecontext;
2000-09-11, by wenzelm
added THIS;
2000-09-11, by wenzelm
case args: align_right;
2000-09-11, by wenzelm
added \isabellecontext;
2000-09-11, by wenzelm
tidied
2000-09-11, by paulson
*** empty log message ***
2000-09-08, by wenzelm
internalize error "insufficient syntax for prefix application";
2000-09-07, by wenzelm
tuned ML code (the_context, bind_thms(s));
2000-09-07, by wenzelm
HOL: qed_spec_mp now also removes bounded ALL;
2000-09-07, by wenzelm
tuned ML code (the_context, bind_thms(s));
2000-09-07, by wenzelm
updated attribute names;
2000-09-07, by wenzelm
improved att names;
2000-09-07, by wenzelm
use Rulify.rulify_no_asm;
2000-09-07, by wenzelm
print rule: priority;
2000-09-07, by wenzelm
improved att names / msgs;
2000-09-07, by wenzelm
avoid handle_error (better msgs);
2000-09-07, by wenzelm
tuned msgs;
2000-09-07, by wenzelm
tuned att names / msgs;
2000-09-07, by wenzelm
tuned;
2000-09-07, by wenzelm
linorder_cases;
2000-09-07, by wenzelm
chop_nonempty: accomodate new qed_spec_mp;
2000-09-07, by wenzelm
added linorder_cases;
2000-09-07, by wenzelm
eliminated rulify setup (now in Provers/rulify.ML);
2000-09-07, by wenzelm
tuned msg;
2000-09-07, by wenzelm
updated rulify setup;
2000-09-07, by wenzelm
added Provers/rulify;
2000-09-07, by wenzelm
removed rulify_attrib_setup;
2000-09-07, by wenzelm
rulify setup;
2000-09-07, by wenzelm
added Provers/rulify.ML;
2000-09-07, by wenzelm
eliminated rulify stuff (now in Provers/rulify.ML);
2000-09-07, by wenzelm
updated setup;
2000-09-07, by wenzelm
setup Rulify.setup;
2000-09-07, by wenzelm
Conversion of object-level -->/ALL into meta-level ==>/!!;
2000-09-07, by wenzelm
a number of new theorems
2000-09-07, by paulson
Added meaningful output to cong-error msg.
2000-09-07, by nipkow
strengthened dvd_mod & proofed dvd_mod_iff
2000-09-07, by paulson
tuned;
2000-09-06, by wenzelm
make SML/NJ happy;
2000-09-06, by wenzelm
fixed structure U;
2000-09-06, by wenzelm
less_induct -> nat_less_induct
2000-09-06, by nipkow
tuned;
2000-09-06, by wenzelm
imp_cong bound at thm level.
2000-09-06, by nipkow
bug fix for arithmetic simprocs (nat & int)
2000-09-06, by paulson
tidied
2000-09-06, by paulson
new Iff theorem zero_le_succ_iff
2000-09-06, by paulson
*** empty log message ***
2000-09-06, by nipkow
less_induct -> nat_less_induct
2000-09-06, by nipkow
improved meson setup;
2000-09-05, by wenzelm
fixed quotes;
2000-09-05, by wenzelm
tuned;
2000-09-05, by wenzelm
proper handling of hints;
2000-09-05, by wenzelm
eliminated;
2000-09-05, by wenzelm
generalized types of args;
2000-09-05, by wenzelm
tuned output of isabelle env;
2000-09-05, by wenzelm
improved add_rules;
2000-09-05, by wenzelm
removed 'other' modifier;
2000-09-05, by wenzelm
added 'iff' declarations;
2000-09-05, by wenzelm
recdef hints (attributes and modifiers);
2000-09-05, by wenzelm
use 'iff' modifier;
2000-09-05, by wenzelm
RecdefPackage.add_recdef_old;
2000-09-05, by wenzelm
added not_const;
2000-09-05, by wenzelm
improved recdef setup;
2000-09-05, by wenzelm
lemmas [recdef_cong] = map_cong;
2000-09-05, by wenzelm
removed Add_recdef_congs [map_cong] (see Main.thy);
2000-09-05, by wenzelm
tuned setup;
2000-09-05, by wenzelm
iff declarations moved to clasimp.ML;
2000-09-05, by wenzelm
added not;
2000-09-05, by wenzelm
simplified PG/X-Symbol intro;
2000-09-05, by wenzelm
recdef hints (attributes and modifiers);
2000-09-05, by wenzelm
added 'iff' modifier;
2000-09-05, by wenzelm
tuned;
2000-09-05, by wenzelm
updated;
2000-09-05, by wenzelm
*** empty log message ***
2000-09-05, by nipkow
tidied, proving gcd_greatest_iff and using induct_tac
2000-09-05, by paulson
new AddIffs (especially Memrel_iff)
2000-09-05, by paulson
safe_meson_tac -> meson_tac
2000-09-05, by paulson
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
2000-09-05, by paulson
loads Tools/meson.ML: meson_tac installed by default
2000-09-05, by paulson
moved proof of "choice" to Tools/meson.ML
2000-09-05, by paulson
fixed a slow proof
2000-09-05, by paulson
simplified two index entries, since now ZF is by itself
2000-09-05, by paulson
meson_tac
2000-09-05, by paulson
*** empty log message ***
2000-09-05, by nipkow
tuned comment;
2000-09-04, by wenzelm
added safe_mk_meta_eq;
2000-09-04, by wenzelm
tuned "mono" att setup;
2000-09-04, by wenzelm
tuned;
2000-09-04, by wenzelm
added add_rules, del_rules;
2000-09-04, by wenzelm
display: avoid empty lines;
2000-09-04, by wenzelm
tuned;
2000-09-04, by wenzelm
minor fixes for new version of Primes.thy
2000-09-04, by paulson
Renamed real_of_posnat_less_zero to real_of_posnat_gt_zero
2000-09-04, by paulson
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
2000-09-04, by paulson
BCV
2000-09-04, by nipkow
added pretend_use_thy_only;
2000-09-03, by wenzelm
proper_inform_file_processed: ThyInfo.pretend_use_thy_only;
2000-09-03, by wenzelm
improved section markup;
2000-09-03, by wenzelm
tuned;
2000-09-03, by wenzelm
GPLed;
2000-09-03, by wenzelm
GPLed;
2000-09-03, by wenzelm
new reference girard89
2000-09-03, by paulson
Lambda/document/root.tex;
2000-09-02, by wenzelm
* HOL/Lambda: converted into new-style theory and document;
2000-09-02, by wenzelm
document setup;
2000-09-02, by wenzelm
updated;
2000-09-02, by wenzelm
HOL/Lambda: converted into new-style theory and document;
2000-09-02, by wenzelm
method_setup: thms closure;
2000-09-02, by wenzelm
added mode parser;
2000-09-02, by wenzelm
added get_thm_closure;
2000-09-02, by wenzelm
"split": added "(asm)" option;
2000-09-02, by wenzelm
added "slow";
2000-09-02, by wenzelm
added "slowsimp", "bestsimp";
2000-09-02, by wenzelm
"inductive_cases": proper command;
2000-09-02, by wenzelm
use Args.mode;
2000-09-02, by wenzelm
converted;
2000-09-02, by wenzelm
added 'iff del' att;
2000-09-02, by wenzelm
tuned rail;
2000-09-02, by wenzelm
'split' method: '(asm)' option;
2000-09-02, by wenzelm
some stuff;
2000-09-02, by wenzelm
provide "--" argument: tentative release;
2000-09-02, by wenzelm
tuned;
2000-09-02, by wenzelm
copy_files: do not quote paths (for now);
2000-09-01, by wenzelm
fixed quoting;
2000-09-01, by wenzelm
isatool nonascii;
2000-09-01, by wenzelm
*** empty log message ***
2000-09-01, by nipkow
Completely new version of BCV
2000-09-01, by nipkow
ISABELLE_PATH: ML_IDENTIFIER no longer added;
2000-09-01, by wenzelm
GPLed;
2000-09-01, by wenzelm
GPLed;
2000-09-01, by wenzelm
more robust handling of spaces in args / file names;
2000-09-01, by wenzelm
GPLed;
2000-09-01, by wenzelm
isatool_document: quote args;
2000-09-01, by wenzelm
export quote_sysify_path;
2000-09-01, by wenzelm
/usr/bin/perl;
2000-09-01, by wenzelm
cleanup dist sources afterwards;
2000-09-01, by wenzelm
cvs-copy - make copy of CVS controlled directory hierarchy;
2000-09-01, by wenzelm
added 'safe' method;
2000-09-01, by wenzelm
Method.bang_sectioned_args';
2000-09-01, by wenzelm
replaced writeln by priority;
2000-09-01, by wenzelm
added bang_sectioned_args';
2000-09-01, by wenzelm
'declare' made proper command;
2000-09-01, by wenzelm
priority_fn := decorate_lines;
2000-09-01, by wenzelm
added priority, priority_fn;
2000-09-01, by wenzelm
added "safe" method;
2000-09-01, by wenzelm
auto method: opt args;
2000-09-01, by wenzelm
converted Lambda scripts;
2000-09-01, by wenzelm
converted;
2000-09-01, by wenzelm
fixed rulify_prems;
2000-09-01, by wenzelm
lemmas [mono] = lists_mono;
2000-09-01, by wenzelm
updated;
2000-09-01, by wenzelm
fixed make_pp;
2000-08-31, by wenzelm
improved exit function for polyml-4.0;
2000-08-31, by wenzelm
tuned
2000-08-31, by kleing
*** empty log message ***
2000-08-31, by nipkow
ported HOL/Lambda/ListBeta;
2000-08-31, by wenzelm
improved handling of messages: do not decorate writeln output;
2000-08-31, by wenzelm
improved messages;
2000-08-31, by wenzelm
more polyml choices;
2000-08-31, by wenzelm
added some bind_thm
2000-08-30, by kleing
functional LBV style, dead code, type safety -> Isar
2000-08-30, by kleing
MicroJava changed (all of BV -> Isar)
2000-08-30, by kleing
tuned
2000-08-30, by kleing
*** empty log message ***
2000-08-30, by nipkow
tuned;
2000-08-30, by wenzelm
renamed antiquotation 'name' to 'text';
2000-08-30, by wenzelm
tuned;
2000-08-30, by wenzelm
added "source" option;
2000-08-30, by wenzelm
token trans: removed \mbox to achieve proper italic correction;
2000-08-30, by wenzelm
added string_of;
2000-08-30, by wenzelm
introduced induct_thm_tac
2000-08-30, by nipkow
*** empty log message ***
2000-08-30, by nipkow
tuned;
2000-08-30, by wenzelm
use polyml-version;
2000-08-30, by wenzelm
*** empty log message ***
2000-08-30, by nipkow
*** empty log message ***
2000-08-30, by nipkow
fixed name;
2000-08-30, by wenzelm
New function name_of_typ.
2000-08-30, by berghofe
Improved names for size function.
2000-08-30, by berghofe
fixed comment;
2000-08-30, by wenzelm
*** empty log message ***
2000-08-30, by nipkow
Fixed rulify.
2000-08-30, by nipkow
added ML-Systems/polyml-4.0.ML;
2000-08-29, by wenzelm
added \<dots> syntax;
2000-08-29, by wenzelm
added prems_limit;
2000-08-29, by wenzelm
added "name" antiq and "indent" option;
2000-08-29, by wenzelm
pr: added prems limit;
2000-08-29, by wenzelm
added indent;
2000-08-29, by wenzelm
\<dots> syntax;
2000-08-29, by wenzelm
added antiquotation 'name' and option 'indent';
2000-08-29, by wenzelm
'syntax': improved mode spec;
2000-08-29, by wenzelm
improved spacing of Sum, Prod, integral;
2000-08-29, by wenzelm
underscore: added \mbox to avoid hyphenation;
2000-08-29, by wenzelm
* 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-29, by wenzelm
*** empty log message ***
2000-08-29, by nipkow
*** empty log message ***
2000-08-29, by nipkow
*** empty log message ***
2000-08-29, by nipkow
made SML/XL happy;
2000-08-29, by wenzelm
updated;
2000-08-29, by wenzelm
improved isabellepar env;
2000-08-29, by wenzelm
updated;
2000-08-29, by wenzelm
Lambda/InductTermi made new-style theory;
2000-08-29, by wenzelm
proper cong setup;
2000-08-29, by wenzelm
Simplifier.cong_add_global;
2000-08-29, by wenzelm
cong setup now part of Simplifier;
2000-08-29, by wenzelm
updated cong stuff;
2000-08-29, by wenzelm
'cong' modifiers;
2000-08-29, by wenzelm
\isakeywordcharunderscore;
2000-08-29, by wenzelm
* Isar/Provers: 'simp' method now supports 'cong' modifiers;
2000-08-29, by wenzelm
tex_index: Latex.tex_trailer;
2000-08-28, by wenzelm
added tex_trailer;
2000-08-28, by wenzelm
removed METHOD0;
2000-08-28, by wenzelm
Method.SIMPLE_METHOD';
2000-08-28, by wenzelm
'induct_tac' / 'case_tac': Method.goal_args';
2000-08-28, by wenzelm
added 'split' method;
2000-08-28, by wenzelm
\newenvironment{isabellebody}: version without trivlist;
2000-08-28, by wenzelm
* \isabellestyle{it} produces near math mode output;
2000-08-28, by wenzelm
Removed map_compose from simpset.
2000-08-28, by nipkow
fixed Id string
2000-08-28, by kleing
updated;
2000-08-28, by wenzelm
restart_loader: reset_path;
2000-08-28, by wenzelm
add_path: del_path first;
2000-08-28, by wenzelm
proper setup of iman.sty/extra.sty/ttbox.sty;
2000-08-28, by wenzelm
updated;
2000-08-28, by wenzelm
moved \tt things to ttbox.sty;
2000-08-28, by wenzelm
proper setup;
2000-08-28, by wenzelm
removed ttbox;
2000-08-28, by wenzelm
*** empty log message ***
2000-08-28, by nipkow
*** empty log message ***
2000-08-28, by nipkow
added \trivlist...\endtrivlist to the "isabelle" environment
2000-08-25, by paulson
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
2000-08-25, by paulson
xsymbols for {| and |}
2000-08-24, by paulson
xsymbols for leads-to and Join
2000-08-24, by paulson
fixed strip_assums and assum_pairs, restoring them (essentially) to their
2000-08-24, by paulson
added some xsymbols, and tidied
2000-08-24, by paulson
more symbols;
2000-08-24, by wenzelm
disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);
2000-08-24, by wenzelm
choosefrom: support easy settings;
2000-08-24, by wenzelm
choosefrom: easy settings;
2000-08-24, by wenzelm
isabelle env: trivlist;
2000-08-23, by wenzelm
removed redundant commands
2000-08-22, by paulson
removed most "makeatother", no longer needed
2000-08-22, by paulson
updated to latest versions of ttbox and ttbreak
2000-08-22, by paulson
updated;
2000-08-21, by wenzelm
updated;
2000-08-21, by wenzelm
updated;
2000-08-21, by wenzelm
tuned translations;
2000-08-21, by wenzelm
*** empty log message ***
2000-08-21, by nipkow
added \isastyleminor;
2000-08-21, by wenzelm
more \isachars;
2000-08-21, by wenzelm
fixed has_meta_prems: strip_assums_hyp;
2000-08-21, by wenzelm
*** empty log message ***
2000-08-21, by nipkow
updated;
2000-08-21, by wenzelm
open cases;
2000-08-20, by wenzelm
output \isachar;
2000-08-19, by wenzelm
cond_add_path;
2000-08-19, by wenzelm
fixed text;
2000-08-19, by wenzelm
turned into new-style theory;
2000-08-19, by wenzelm
tuned;
2000-08-19, by wenzelm
tuned \isastyle;
2000-08-19, by wenzelm
added \isachar definitions;
2000-08-19, by wenzelm
%\urlstyle{rm}
2000-08-19, by wenzelm
renamed cond_with_path to cond_add_path (add to front);
2000-08-19, by wenzelm
X-symbols for ordinal, cardinal, integer arithmetic
2000-08-18, by paulson
fixed RuleCases.make (invert flag);
2000-08-18, by wenzelm
removed obsolete add_recdef_x;
2000-08-18, by wenzelm
proper handling of defs;
2000-08-18, by wenzelm
Main now new-style theory; added Main.ML for compatibility;
2000-08-18, by wenzelm
simproc bug fix: only TYPING assumptions are given to the simplifier
2000-08-18, by paulson
better rules for cancellation of common factors across comparisons
2000-08-18, by paulson
new example ZF/ex/NatSum
2000-08-18, by paulson
now allows dest_coeff to fail
2000-08-18, by paulson
*** empty log message ***
2000-08-18, by nipkow
*** empty log message ***
2000-08-18, by nipkow
removed obsolete keyword;
2000-08-17, by wenzelm
fixed indexing;
2000-08-17, by wenzelm
tuned;
2000-08-17, by wenzelm
installed recdef congs data
2000-08-17, by nipkow
added map_cong to recdef
2000-08-17, by nipkow
removed Lambda/Type.ML;
2000-08-17, by wenzelm
better rules for cancellation of common factors across comparisons
2000-08-17, by paulson
fixed a proof that had stopped working ???
2000-08-17, by paulson
tidied & updated proofs, deleting some unused ones
2000-08-17, by paulson
modified proofs: better rules for cancellation of common factors across comparisons
2000-08-17, by paulson
better rules for cancellation of common factors across comparisons
2000-08-17, by paulson
*** empty log message ***
2000-08-17, by wenzelm
cases: opaque by default;
2000-08-17, by wenzelm
renamed 'RS' to 'THEN';
2000-08-17, by wenzelm
tuned error handling;
2000-08-17, by wenzelm
added 'symmetric' attribute;
2000-08-17, by wenzelm
updated;
2000-08-17, by wenzelm
sel_upd proc: include 'more' pseudo-field;
2000-08-17, by wenzelm
renamed 'mk_cases_tac' to 'ind_cases';
2000-08-17, by wenzelm
changed 'opaque' option to 'open' (opaque is default);
2000-08-17, by wenzelm
renamed 'RS' to 'THEN';
2000-08-17, by wenzelm
converted to new-style theory;
2000-08-17, by wenzelm
done;
2000-08-17, by wenzelm
'symmetric' attribute;
2000-08-17, by wenzelm
fixed deps;
2000-08-17, by wenzelm
renamed 'RS' to 'THEN';
2000-08-17, by wenzelm
index tokens;
2000-08-17, by wenzelm
cases/induct method: 'opaque' by default; added 'open' option;
2000-08-17, by wenzelm
updated;
2000-08-17, by wenzelm
renamed 'RS' to 'THEN';
2000-08-17, by wenzelm
fixed lbrace, rbrace;
2000-08-17, by wenzelm
Isar/Pure: renamed 'RS' attribute to 'THEN';
2000-08-17, by wenzelm
Fixed completeness bug in simplifier: congruence rules could preclude
2000-08-16, by nipkow
major sharpening of stable_project_transient
2000-08-16, by paulson
new (unused) lemma
2000-08-16, by paulson
new thm and simprule Compl_Diff_eq
2000-08-16, by paulson
added conversion.tex;
2000-08-14, by wenzelm
moved tactic emulation methods here;
2000-08-14, by wenzelm
added 'declare' command;
2000-08-14, by wenzelm
tuned;
2000-08-14, by wenzelm
updated;
2000-08-14, by wenzelm
renamed 'intrs' to 'intros';
2000-08-14, by wenzelm
updated command termination issue;
2000-08-14, by wenzelm
some more refs;
2000-08-14, by wenzelm
Aspinall:2000:eProof;
2000-08-14, by wenzelm
raplaced "intrs" by "intrs" (new-style only);
2000-08-14, by wenzelm
cases: support multiple insts;
2000-08-14, by wenzelm
intros;
2000-08-14, by wenzelm
added MicroJava/BV/StepMono.thy,
2000-08-14, by kleing
Convert.thy now in Isar, tuned
2000-08-14, by kleing
tuned names;
2000-08-14, by wenzelm
added hypsubst;
2000-08-14, by wenzelm
added "fastsimp";
2000-08-14, by wenzelm
added declare_theorems(_i);
2000-08-14, by wenzelm
added "declare" command;
2000-08-14, by wenzelm
added thy_script kind;
2000-08-14, by wenzelm
tuned msg;
2000-08-14, by wenzelm
use_let: exclude 'val';
2000-08-14, by wenzelm
fixed document preparation;
2000-08-14, by wenzelm
documented the integers and updated section on nat arithmetic
2000-08-12, by paulson
some ad-hoc simprules for div and mod to reduce the
2000-08-12, by paulson
deleted needless rules
2000-08-12, by paulson
added bind_thm for widen_RefT etc.
2000-08-11, by kleing
tuned
2000-08-11, by kleing
added LBV
2000-08-11, by kleing
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
2000-08-11, by paulson
ZF arith
2000-08-11, by paulson
interim working version: more improvements to the integers
2000-08-11, by paulson
Equations that are added to the simpset now have proper names.
2000-08-10, by berghofe
new structure field "add" for CombineNumerals
2000-08-10, by paulson
the "nocheck" versions of goal functions now standardize their result
2000-08-10, by paulson
tidied
2000-08-10, by paulson
new structure field "add" for CombineNumerals
2000-08-10, by paulson
installation of cancellation simprocs for the integers
2000-08-10, by paulson
X-Symbol mode -- look in canonical place;
2000-08-10, by wenzelm
fixed spelling;
2000-08-09, by wenzelm
added Bauer-Wenzel:2000:HB;
2000-08-09, by wenzelm
thms closure;
2000-08-09, by wenzelm
res_inst: include non-inst versions with multiple thms;
2000-08-09, by wenzelm
added get_thms_closure, single_thm;
2000-08-09, by wenzelm
fixed classification of rules in atts and modifiers (final!?);
2000-08-09, by wenzelm
fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;
2000-08-09, by wenzelm
thms "atomize";
2000-08-09, by wenzelm
tuned;
2000-08-09, by bauerg
tuned
2000-08-09, by kleing
token translation: enclose "\\mbox{" "}";
2000-08-08, by wenzelm
added Example
2000-08-08, by oheimb
moved Hoare_example to Examples; other minor improvements
2000-08-08, by oheimb
Deleted unneeded proof; simplified proof of app_last.
2000-08-08, by berghofe
added forall_elim_vars_safe, norm_hhf_eq;
2000-08-08, by wenzelm
norm_hhf results;
2000-08-08, by wenzelm
prf_heading kind;
2000-08-08, by wenzelm
MicroJava structure changed
2000-08-07, by kleing
Invoke instruction gets fully qualified method name (class+name+sig) as
2000-08-07, by kleing
BV and LBV specified in terms of app and step functions
2000-08-07, by kleing
instantiated Cancel_Numerals for "nat" in ZF
2000-08-07, by paulson
more cterm operations: mk_implies, list_implies
2000-08-07, by paulson
prove_conv gets an extra argument, so the ZF instantiation can use hyps
2000-08-07, by paulson
tidied
2000-08-07, by paulson
added a dummy "thm list" argument to prove_conv for the new interface to
2000-08-07, by paulson
new abstract syntax operations, used in ZF
2000-08-07, by paulson
ZF arith
2000-08-07, by paulson
*** empty log message ***
2000-08-06, by nipkow
dummy_patterns moved to term.ML;
2000-08-04, by wenzelm
added goal_args(');
2000-08-04, by wenzelm
added int;
2000-08-04, by wenzelm
axioms: Term.no_dummy_patterns;
2000-08-04, by wenzelm
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
2000-08-04, by wenzelm
added rename_params_tac;
2000-08-04, by wenzelm
dummy_pattern moved to term.ML;
2000-08-04, by wenzelm
Term.no_dummy_patterns;
2000-08-04, by wenzelm
added rev_eq_reflection;
2000-08-04, by wenzelm
val rev_eq_reflection = def_imp_eq;
2000-08-04, by wenzelm
val atomize = thms "atomize";
2000-08-04, by wenzelm
lemmas atomize = all_eq imp_eq;
2000-08-04, by wenzelm
rev_eq_reflection = meta_eq_to_obj_eq;
2000-08-04, by wenzelm
removed stac (now exported by HypsubstFun);
2000-08-04, by wenzelm
setup hypsubst_setup;
2000-08-04, by wenzelm
lemmas atomize = all_eq imp_eq;
2000-08-04, by wenzelm
added rev_eq_reflection;
2000-08-04, by wenzelm
subgoals_tac: fixed spelling;
2000-08-04, by wenzelm
invoke isatool make in any dir containing an IsaMakefile;
2000-08-04, by wenzelm
updated;
2000-08-04, by wenzelm
targets for images, test, all;
2000-08-04, by wenzelm
updated;
2000-08-04, by wenzelm
tuned;
2000-08-04, by wenzelm
tuned version by Stephan Merz (unbatchified etc.);
2000-08-03, by wenzelm
tuned TLA;
2000-08-03, by wenzelm
added setmp_verbose;
2000-08-03, by wenzelm
tuned;
2000-08-03, by wenzelm
unknown_theory/proof/context;
2000-08-03, by wenzelm
added unknown_theory/proof/context;
2000-08-03, by wenzelm
new theorem neq_commute
2000-08-03, by paulson
new files Integ/IntPower.{thy.ML}; tidied
2000-08-03, by paulson
introduction of integer exponentiation
2000-08-03, by paulson
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
2000-08-03, by paulson
GPLed;
2000-08-03, by wenzelm
export get_local_clasimpset, clasimp_modifiers;
2000-08-03, by wenzelm
improved output of space symbol;
2000-08-03, by wenzelm
typ_no_norm;
2000-08-03, by wenzelm
tuned;
2000-08-03, by wenzelm
adapted deriv;
2000-08-02, by wenzelm
derivations: maintain oracle flag;
2000-08-02, by wenzelm
use oracle flag from derivation;
2000-08-02, by wenzelm
rep_thm: 'der' field has additional bool for oracles;
2000-08-02, by wenzelm
minor corrections
2000-08-02, by oheimb
isa: do not touch_all_thys on startup;
2000-08-02, by wenzelm
coercion "intify" to remove type constraints from integer algebraic laws
2000-08-02, by paulson
tidying and speeding up proofs
2000-08-02, by paulson
*** empty log message ***
2000-08-02, by nipkow
*** empty log message ***
2000-08-02, by nipkow
used natify with div and mod; also put in the divide-by-zero trick
2000-08-01, by paulson
natify, a coercion to reduce the number of type constraints in arithmetic
2000-08-01, by paulson
tuned msg;
2000-08-01, by wenzelm
* blast(_tac) now handles actual object-logic rules as assumptions;
2000-08-01, by wenzelm
added all_eq, imp_eq (for blast);
2000-08-01, by wenzelm
improved comments;
2000-08-01, by wenzelm
handle actual object-logic rules by atomizing the goal;
2000-08-01, by wenzelm
added atomize_goal / atomize_tac;
2000-08-01, by wenzelm
(un)fold: CHANGED;
2000-08-01, by wenzelm
added has_meta_prems;
2000-08-01, by wenzelm
tuned;
2000-08-01, by wenzelm
tuned;
2000-07-31, by wenzelm
updated 'obtain';
2000-07-31, by wenzelm
Removed Quot
2000-07-31, by nipkow
Never used and not relevant.
2000-07-31, by nipkow
obtain;
2000-07-30, by wenzelm
added split_bind_asm, bind_splits;
2000-07-30, by wenzelm
adapted obtain;
2000-07-30, by wenzelm
removed equalityCE;
2000-07-30, by wenzelm
added atomic_Trueprop;
2000-07-30, by wenzelm
updated ObtainFun;
2000-07-30, by wenzelm
'def': no constraint on variable;
2000-07-30, by wenzelm
exporter setup for context elements;
2000-07-30, by wenzelm
export RANGE, hard_asm_tac, soft_asm_tac;
2000-07-30, by wenzelm
turned into plain context element;
2000-07-30, by wenzelm
local_def(_i): no constraint on var;
2000-07-30, by wenzelm
local_def(_i): no constraint on var;
2000-07-30, by wenzelm
def: no constraint on var;
2000-07-30, by wenzelm
added is_judgment;
2000-07-30, by wenzelm
ObtainFun (generalized existence reasoning);
2000-07-30, by wenzelm
ThmDeps.enable;
2000-07-30, by wenzelm
added sign_of_cterm;
2000-07-30, by wenzelm
Logic.goal_const;
2000-07-30, by wenzelm
replaced "Sessions" by "Root";
2000-07-28, by wenzelm
apply. -> by
2000-07-28, by nipkow
* HOL/While
2000-07-28, by nipkow
added theory While;
2000-07-27, by wenzelm
export has_internal;
2000-07-27, by wenzelm
added thm_deps;
2000-07-27, by wenzelm
added enter_forward_proof;
2000-07-27, by wenzelm
export write_graph;
2000-07-27, by wenzelm
begin_theory: store *copy* of initial theory;
2000-07-27, by wenzelm
tuned;
2000-07-27, by wenzelm
intro_elim_tac: bimatch_from;
2000-07-27, by wenzelm
While functional for defining tail-recursive functions
2000-07-26, by nipkow
*** empty log message ***
2000-07-26, by nipkow
tuned msg;
2000-07-25, by wenzelm
Corrected example which still used old primrec syntax.
2000-07-25, by berghofe
Replaced force by fast because force may now take forever to fail
2000-07-25, by nipkow
new constant same_fst
2000-07-25, by nipkow
by (CLASIMPSET auto_tac);
2000-07-25, by wenzelm
added clarify method;
2000-07-25, by wenzelm
added clarsimp method;
2000-07-25, by wenzelm
tuned;
2000-07-25, by wenzelm
removed slow, slow_best methods;
2000-07-25, by wenzelm
* Isar/Provers: intro/elim/dest attributes: changed
2000-07-25, by wenzelm
rearranged setup of arithmetic procedures, avoiding global reference values;
2000-07-25, by wenzelm
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
2000-07-25, by wenzelm
do nat pass theory value, but sg_ref;
2000-07-25, by wenzelm
avoid referencing thy value;
2000-07-25, by wenzelm
avoid referencing thy value;
2000-07-25, by wenzelm
tuned deps;
2000-07-25, by wenzelm
tuned;
2000-07-24, by wenzelm
changed deps;
2000-07-24, by wenzelm
rename_numerals: use implicit theory context;
2000-07-24, by wenzelm
avoid referencing thy value;
2000-07-24, by wenzelm
avoid referencing thy value;
2000-07-24, by wenzelm
avoid referencing thy value;
2000-07-24, by wenzelm
simpset_of NatDef.thy (why anyway?);
2000-07-24, by wenzelm
avoid referencing thy value;
2000-07-24, by wenzelm
avoid referencing thy value;
2000-07-24, by wenzelm
tuned comment;
2000-07-24, by wenzelm
avoid global references;
2000-07-24, by wenzelm
do not pass theory values, but sg_ref;
2000-07-24, by wenzelm
Drule.merge_rules;
2000-07-24, by wenzelm
get_names: topologically sorted;
2000-07-23, by wenzelm
removed all_sessions.graph;
2000-07-23, by wenzelm
removed all_sessions;
2000-07-23, by wenzelm
disallow duplicates in session identifiers;
2000-07-23, by wenzelm
assimilated;
2000-07-23, by wenzelm
tuned HeapFun;
2000-07-23, by wenzelm
tuned ThmHeap;
2000-07-23, by wenzelm
removed selector syntax -- improper tuples are broken beyond repair :-(
2000-07-23, by wenzelm
elim?;
2000-07-23, by wenzelm
classical atts now intro! / intro / intro?;
2000-07-23, by wenzelm
renamed "Directories" to "Sessions";
2000-07-23, by wenzelm
tuned;
2000-07-23, by wenzelm
improved error msg;
2000-07-22, by wenzelm
added ex_someI
2000-07-21, by nipkow
much tidying in connection with the 2nd UNITY paper
2000-07-21, by paulson
strengthened force_tac by using new first_best_tac
2000-07-21, by oheimb
removed safe_asm_full_simp_tac
2000-07-21, by oheimb
added map_upd_nonempty, also to simpset
2000-07-21, by oheimb
removed weaker variant of subset_insert_iff
2000-07-21, by oheimb
removed safe_asm_full_simp_tac, added generic_simp_tac
2000-07-21, by oheimb
Updating of some comments
2000-07-21, by prensani
*** empty log message ***
2000-07-21, by nipkow
Univ no longer requires Arith (really it never did)
2000-07-21, by paulson
tuned;
2000-07-20, by wenzelm
corrected header
2000-07-19, by oheimb
changed / to // for quotienting
2000-07-19, by paulson
changed / to // for quotienting; general tidying
2000-07-19, by paulson
renamed // to / (which is what we want anyway) to avoid clash with the new
2000-07-19, by paulson
deleted redundant proof
2000-07-19, by paulson
// change; also moved entry for AddIffs
2000-07-19, by paulson
addsplits [split_if];
2000-07-18, by wenzelm
theorems foo.splits = foo.split foo.split_asm;
2000-07-18, by wenzelm
removed obsolete expand_if = split_if;
2000-07-18, by wenzelm
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
2000-07-18, by wenzelm
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
2000-07-18, by wenzelm
replaced arities by instance;
2000-07-18, by wenzelm
MicroJava structure changed
2000-07-18, by kleing
consts: include *all* names;
2000-07-17, by wenzelm
tuded presentation;
2000-07-17, by bauerg
AddXIs [UnI1, UnI2];
2000-07-17, by wenzelm
flat instruction set, op. semantics now in JVMExecInstr.thy
2000-07-17, by kleing
flat instruction set
2000-07-17, by kleing
10pt
2000-07-17, by bauerg
- xsymbols for
2000-07-17, by bauerg
strip_prod_type = HOLogic.prodT_factors;
2000-07-16, by wenzelm
AST translation rules no longer require constant head on LHS;
2000-07-16, by wenzelm
fixed nested prod syntax;
2000-07-16, by wenzelm
use split_tupled_all;
2000-07-16, by wenzelm
use pair_tac;
2000-07-16, by wenzelm
adapted tuple syntax;
2000-07-16, by wenzelm
tuned;
2000-07-16, by wenzelm
use pair_tac;
2000-07-16, by wenzelm
use split syntax;
2000-07-16, by wenzelm
fixed tuple translations;
2000-07-16, by wenzelm
defs (overloaded);
2000-07-16, by wenzelm
added is_unitT;
2000-07-16, by wenzelm
instance unit :: finite;
2000-07-16, by wenzelm
more robust tuple syntax (still improper, though!);
2000-07-16, by wenzelm
improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac;
2000-07-16, by wenzelm
added syntax for proper / improper selector functions;
2000-07-16, by wenzelm
tuned;
2000-07-16, by wenzelm
tuned;
2000-07-16, by wenzelm
avoid 'split';
2000-07-16, by wenzelm
added Tuple.thy;
2000-07-16, by wenzelm
added ex/Tuple.thy;
2000-07-16, by wenzelm
syntax (symbols) "op o" moved from HOL to Fun;
2000-07-16, by wenzelm
added finite_unit;
2000-07-16, by wenzelm
AST translation rules no longer require constant head on LHS;
2000-07-16, by wenzelm
* tuned AST representation of nested pairs, avoiding bogus output in
2000-07-16, by wenzelm
corrections (cast relation, Prog.ML -> Decl.ML)
2000-07-14, by oheimb
improved add_edges_cyclic;
2000-07-14, by wenzelm
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
2000-07-14, by oheimb
added (surjective_pairing RS sym) to simpset
2000-07-14, by oheimb
strengthened rtranclD
2000-07-14, by oheimb
added option_map_o_sum_case (also to simpset)
2000-07-14, by oheimb
added sum_case_empty_empty (also to simpset)
2000-07-14, by oheimb
tuned syntax
2000-07-14, by oheimb
added hint on fun_sum
2000-07-14, by oheimb
added fun_upd2_simproc
2000-07-14, by oheimb
re-added subset_empty to simpset
2000-07-14, by oheimb
used bounded quantification in definition of guarantees and other minor
2000-07-14, by paulson
moved sublist from UNITY/AllocBase to List
2000-07-14, by paulson
AddIffs
2000-07-14, by paulson
parent should be Main
2000-07-14, by paulson
changed the quotient syntax from / to //
2000-07-14, by paulson
tuned cycle_msg;
2000-07-13, by wenzelm
updated;
2000-07-13, by wenzelm
HOL: the disjoint sum is now "<+>" instead of "Plus";
2000-07-13, by wenzelm
adapted PureThy.add_defs_i;
2000-07-13, by wenzelm
defs (overloaded);
2000-07-13, by wenzelm
tuned;
2000-07-13, by wenzelm
added read_xnum;
2000-07-13, by wenzelm
fix(_i): admit internal variables;
2000-07-13, by wenzelm
use ProofContext.bind_skolem;
2000-07-13, by wenzelm
defs: (overloaded) option;
2000-07-13, by wenzelm
eq_prop: strip_assums_concl;
2000-07-13, by wenzelm
tuned exceptions;
2000-07-13, by wenzelm
const_deps: unit Graph.T;
2000-07-13, by wenzelm
add_term_consts: ins_string;
2000-07-13, by wenzelm
add_defs(_i): overloaded option;
2000-07-13, by wenzelm
adapted PureThy.add_defs;
2000-07-13, by wenzelm
fixed comment;
2000-07-13, by wenzelm
adapted PureThy.add_defs_i;
2000-07-13, by wenzelm
use Syntax.read_xnum;
2000-07-13, by wenzelm
fixed simplified_cases;
2000-07-13, by wenzelm
fixed name: UN_empty3;
2000-07-13, by wenzelm
replaced infix Plus by <+>;
2000-07-13, by wenzelm
removed duplicate Compl_atMost;
2000-07-13, by wenzelm
fixed compose decl;
2000-07-13, by wenzelm
defs: (overloaded) option;
2000-07-13, by wenzelm
method cases/induct: (opaque) option;
2000-07-13, by wenzelm
defs (overloaded);
2000-07-13, by wenzelm
removed now-redundant proof steps
2000-07-13, by paulson
added an important default rule
2000-07-13, by paulson
fixed a failing proof
2000-07-13, by paulson
le_refl_iff as default rule
2000-07-13, by paulson
removed needless premises
2000-07-13, by paulson
AddIffs now available for FOL, ZF
2000-07-13, by paulson
added simp_case_tac;
2000-07-13, by wenzelm
use InductMethod.simp_case_tac;
2000-07-13, by wenzelm
tuned;
2000-07-13, by wenzelm
export thesisN separately;
2000-07-13, by wenzelm
prep rhs in original context;
2000-07-13, by wenzelm
RuleCases.make opaq;
2000-07-13, by wenzelm
bind_skolem;
2000-07-13, by wenzelm
invoke_case: bind_skolem;
2000-07-13, by wenzelm
"_i" arguments now expected to have skolems already internalized;
2000-07-13, by wenzelm
make: opaq flag;
2000-07-13, by wenzelm
added internal, dest_internal;
2000-07-13, by wenzelm
infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-07-12, by wenzelm
about.html -> logics.html
2000-07-12, by kleing
munich webserver is now sunbroy51
2000-07-12, by kleing
about -> logics, better access to online libraries
2000-07-12, by kleing
removal of (harmless) circular definitions
2000-07-10, by paulson
Tuned proof.
2000-07-09, by berghofe
Defs are now checked for circularity (if not overloaded).
2000-07-08, by nipkow
inter_sort: keep normal!
2000-07-07, by wenzelm
Tightened up check of types in constant defs.
2000-07-07, by nipkow
added type classes to constant's type
2000-07-07, by nipkow
skp; le;
2000-07-07, by bauerg
added dependency caveat
2000-07-07, by oheimb
added dependency caveat
2000-07-07, by oheimb
added IMP/Examples.ML dependence
2000-07-07, by oheimb
tuned msgs;
2000-07-06, by wenzelm
allow comment in more commands;
2000-07-06, by wenzelm
Isabelle99-1;
2000-07-06, by wenzelm
ADD -> IAdd
2000-07-06, by kleing
Removed some junk thms.
2000-07-06, by nipkow
added zabs to arith_tac
2000-07-06, by nipkow
Deleted list_case thms no subsumed by case_tac
2000-07-06, by nipkow
Now two split thms for same constant at different types is allowed.
2000-07-06, by nipkow
removal of batch style, and tidying
2000-07-06, by paulson
removal of batch style, and tidying
2000-07-06, by paulson
removal of batch style, and tidying
2000-07-06, by paulson
removal of batch style, and tidying
2000-07-06, by paulson
removed sorry;
2000-07-06, by bauerg
removed sorry;
2000-07-06, by bauerg
new ADD instruction
2000-07-06, by kleing
removal of batch style, and tidying
2000-07-06, by paulson
fixed typos reported by Jeremy Dawson
2000-07-06, by paulson
added;
2000-07-06, by bauerg
completed TYPES version of HahnBanach;
2000-07-06, by bauerg
*** empty log message ***
2000-07-06, by nipkow
Compatibility file for Moscow ML 2.00;
2000-07-06, by wenzelm
run Moscow ML 2.00 --- does not handle saved images (yet!?);
2000-07-06, by wenzelm
Moscow ML 2.00 or later (experimental!);
2000-07-06, by wenzelm
more tidying. also generalized some tactics to prove "Type A" and
2000-07-05, by paulson
disambiguated := ; added Examples (factorial)
2000-07-05, by oheimb
removed batch proofs
2000-07-05, by paulson
massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-07-05, by paulson
disambiguated := ; added Examples (factorial)
2000-07-05, by oheimb
corrected symbol for casting relation
2000-07-05, by oheimb
removed most batch-style proofs
2000-07-04, by paulson
tuned;
2000-07-04, by wenzelm
disambiguated := ; added Examples (factorial)
2000-07-04, by oheimb
added a thm.
2000-07-04, by nipkow
disambiguated := ; added Examples (factorial)
2000-07-04, by oheimb
added BinOp
2000-07-04, by oheimb
* added 'nothing' --- the empty list of theorems;
2000-07-04, by wenzelm
added "nothing" (empty list of theorems);
2000-07-04, by wenzelm
fixed usage;
2000-07-04, by wenzelm
tuned comments;
2000-07-04, by wenzelm
previde 'defs' field for quick_and_dirty;
2000-07-03, by wenzelm
IGNORE last log message!
2000-07-01, by wenzelm
removed "help";
2000-07-01, by wenzelm
added no_vars att;
2000-07-01, by wenzelm
eta_contract: no default;
2000-07-01, by wenzelm
GPLed;
2000-07-01, by wenzelm
* Isar/HOL/Calculation: new rules for substitution in inequalities
2000-07-01, by wenzelm
added subst rules for ord(er), including monotonicity conditions;
2000-07-01, by wenzelm
added ISABELLE_SITE_SETTINGS_PRESENT;
2000-07-01, by wenzelm
tuned;
2000-07-01, by wenzelm
added site settings check;
2000-07-01, by wenzelm
* Isar: removed 'help' command, which hasn't been too helpful anyway;
2000-07-01, by wenzelm
removed help;
2000-07-01, by wenzelm
removed help_methods;
2000-07-01, by wenzelm
removed "help";
2000-07-01, by wenzelm
added options "eta_contract", "long_names";
2000-07-01, by wenzelm
added print_trans_rules, print_antiquotations;
2000-07-01, by wenzelm
removed help;
2000-07-01, by wenzelm
tuned print_rules;
2000-07-01, by wenzelm
removed help_attributes;
2000-07-01, by wenzelm
print_theorems: omit name space;
2000-07-01, by wenzelm
Defined abs on int.
2000-07-01, by nipkow
help_antiquotations;
2000-06-30, by wenzelm
overloading, axclasses, numerals and general tidying
2000-06-30, by paulson
removal of batch-style proofs
2000-06-30, by paulson
more tidying
2000-06-30, by paulson
presentation: self-contained session dirs;
2000-06-30, by wenzelm
fixed ISABELLE_BROWSER_INFO;
2000-06-30, by wenzelm
removed the mutual recursion from "bin_add"
2000-06-30, by paulson
tidied and deleted two redundant theories
2000-06-30, by paulson
improved arrangement of files;
2000-06-29, by wenzelm
tuned rail setup;
2000-06-29, by wenzelm
added lbrace, rbrace, atsign;
2000-06-29, by wenzelm
added \indexisarant;
2000-06-29, by wenzelm
adapted args of IsarThy.have_theorems_i;
2000-06-29, by wenzelm
syntax: renamed 'thmname' to 'thmbind';
2000-06-29, by wenzelm
facts: support multiple lists of arguments;
2000-06-29, by wenzelm
* formal comments (text blocks etc.) in new-style theories may now
2000-06-29, by wenzelm
added method_setup;
2000-06-29, by wenzelm
facts: handle multiple lists of arguments;
2000-06-29, by wenzelm
fixed is_semicolon (keyword instead of command!);
2000-06-29, by wenzelm
added add_method;
2000-06-29, by wenzelm
have_theorems etc.: handle multiple lists of arguments;
2000-06-29, by wenzelm
have_thmss: handle multiple lists of arguments;
2000-06-29, by wenzelm
now freezes Vars in order to prevent errors in cases like these:
2000-06-29, by paulson
tidied proofs using default rule equalityCE
2000-06-29, by paulson
the default equalityCE simplifies proofs
2000-06-29, by paulson
tidied
2000-06-29, by paulson
fixed proof to cope with the default of equalityCE instead of equalityE
2000-06-29, by paulson
now uses equalityCE, which usually is more efficent than equalityE
2000-06-29, by paulson
weak elimination rules
2000-06-29, by paulson
classical 'elimify' attribute;
2000-06-28, by wenzelm
tuned for ProofGeneral 3.2
2000-06-28, by kleing
tuning, eliminated rev_surj
2000-06-28, by kleing
fixed some weak elim rules, and tidied
2000-06-28, by paulson
tidying and unbatchifying
2000-06-28, by paulson
no longer depends upon a prior "open Ind_Syntax" from elsewhere
2000-06-28, by paulson
fixed some weak elim rules, and tidied
2000-06-28, by paulson
fixed some weak elim rules
2000-06-28, by paulson
simplified slightly by using dependencies better in theories
2000-06-28, by paulson
finally theory Bin (the integers) is included
2000-06-28, by paulson
FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG
2000-06-28, by paulson
fixed some weak elim rules
2000-06-28, by paulson
implements a classical version of make_elim
2000-06-28, by paulson
uses a supplied version of make_elim for addDs
2000-06-28, by paulson
warns of weak elim rules and ignores them
2000-06-28, by paulson
tidying and unbatchifying
2000-06-28, by paulson
fixed some abuses of addDs and addEs
2000-06-28, by paulson
got rid of weak elim rule
2000-06-28, by paulson
tidied
2000-06-28, by paulson
fixed some weak elim rules
2000-06-28, by paulson
make_elim -> cla_make_elim; tidied
2000-06-28, by paulson
updated and tidied
2000-06-28, by paulson
tidied a monstrous proof
2000-06-28, by paulson
deleted a redundant bind_thm
2000-06-28, by paulson
using the new theorem wf_not_refl; tidied
2000-06-28, by paulson
rev_notE now makes strong elim rules;
2000-06-28, by paulson
declaring and using cla_make_elim
2000-06-28, by paulson
new file Provers/make_elim.ML
2000-06-28, by paulson
replaced arities by instance;
2000-06-27, by wenzelm
OuterLex.name_of: include val;
2000-06-27, by wenzelm
excursion_result: transform_error;
2000-06-27, by wenzelm
eq_prop: eta contract;
2000-06-26, by wenzelm
tuned msg;
2000-06-26, by wenzelm
tuned;
2000-06-26, by wenzelm
avoid \< in input;
2000-06-26, by wenzelm
export proper induction rule;
2000-06-26, by wenzelm
bind_thm;
2000-06-26, by wenzelm
corrected specifications and simplified proofs
2000-06-26, by oheimb
isar-strip-terminators;
2000-06-26, by wenzelm
updated;
2000-06-26, by wenzelm
tuned;
2000-06-26, by wenzelm
use with_paths;
2000-06-26, by wenzelm
prefer mp over subst;
2000-06-25, by wenzelm
tuned;
2000-06-25, by wenzelm
Isar theory output.
2000-06-25, by wenzelm
Theory headers (old and new-style).
2000-06-25, by wenzelm
Text with antiquotations of inner items (terms, types etc.).
2000-06-25, by wenzelm
use Library.change;
2000-06-25, by wenzelm
adapted to improved presentation;
2000-06-25, by wenzelm
adapted to improved presentation;
2000-06-25, by wenzelm
excursion_result;
2000-06-25, by wenzelm
added extern_skolem;
2000-06-25, by wenzelm
moved header stuff to thy_header.ML;
2000-06-25, by wenzelm
added semicolon;
2000-06-25, by wenzelm
added !!!;
2000-06-25, by wenzelm
use ThyHeader.args;
2000-06-25, by wenzelm
rearranged print commands;
2000-06-25, by wenzelm
exception OUTPUT_FAIL of (string * Position.T) * exn
2000-06-25, by wenzelm
removed obsolete "{}";
2000-06-25, by wenzelm
added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
2000-06-25, by wenzelm
added IsarOutput (token-level theory output);
2000-06-25, by wenzelm
added exhausted: ('a, 'b) source -> ('a, 'a list) source;
2000-06-25, by wenzelm
added state: 'a * 'b -> 'a * ('a * 'b);
2000-06-25, by wenzelm
fbrk: 2 if not taken;
2000-06-25, by wenzelm
export hidden: string -> string;
2000-06-25, by wenzelm
tuned;
2000-06-25, by wenzelm
added change: 'a ref -> ('a -> 'a) -> unit;
2000-06-25, by wenzelm
Added new theory Lambda/Type.
2000-06-23, by berghofe
get_inductive now returns None instead of raising an exception.
2000-06-23, by berghofe
Added new theory.
2000-06-23, by berghofe
Subject reduction and strong normalization of simply-typed lambda terms.
2000-06-23, by berghofe
new theorem trans_O_subset
2000-06-23, by paulson
added the AllocImpl example
2000-06-23, by paulson
genPrefix_trans_O: generalizes genPrefix_trans
2000-06-23, by paulson
added the allocator refinement proof
2000-06-23, by paulson
sum_below f n -> setsum f (lessThan n)
2000-06-23, by paulson
bind_thm(s);
2000-06-22, by wenzelm
removed some finiteness conditions from bag_of/sublist theorems
2000-06-22, by paulson
working proofs of the basic merge and distributor properties
2000-06-22, by paulson
fixed the merge spec (NbT -> Nclients) and added the distributor spec
2000-06-22, by paulson
new thoerem Always_Follows2; renamed Always_Follows -> Always_Follows1
2000-06-22, by paulson
added with_paths;
2000-06-21, by wenzelm
fixed deps;
2000-06-21, by wenzelm
fixed deps;
2000-06-21, by wenzelm
fixed deps;
2000-06-21, by wenzelm
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
2000-06-21, by paulson
new theorem UN_empty; it and Un_empty inserted by AddIffs
2000-06-21, by paulson
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
2000-06-21, by paulson
tidied; weakened the (impossible) premises of setsum_UN_disjoint
2000-06-21, by paulson
new module for heaps
2000-06-20, by paulson
now uses the heap data structure for BEST_FIRST
2000-06-20, by paulson
new file heap.ML
2000-06-20, by paulson
changed the Schubert Steamroller proof
2000-06-20, by paulson
another brick in the wall
2000-06-20, by paulson
changed a step for the improved rules for setsum
2000-06-20, by paulson
deleted a step made redundant by the improved rules for setsum
2000-06-20, by paulson
replaced the useless [p]subset_insertD by [p]subset_insert_iff
2000-06-20, by paulson
now setsum f A = 0 unless A is finite
2000-06-20, by paulson
now setsum f A = 0 unless A is finite; proved setsum_cong
2000-06-20, by paulson
real simprocs
2000-06-16, by paulson
fixed for removal of subset_empty
2000-06-16, by paulson
this proof needs more detail
2000-06-16, by paulson
uncommented the last 2 examples; tidied
2000-06-16, by paulson
new lemma real_minus_diff_eq
2000-06-16, by paulson
fixed the installation of linear arithmetic for the reals
2000-06-16, by paulson
some missing simprules for integer linear arithmetic
2000-06-16, by paulson
tidied for new card_seteq
2000-06-16, by paulson
subset_empty is no longer a simprule
2000-06-16, by paulson
renamed psubset_card -> psubset_card_mono
2000-06-16, by paulson
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
2000-06-16, by paulson
inserted some "addsimps [subset_empty]"; also tidied (a lot)
2000-06-16, by paulson
tracing flag for arith_tac
2000-06-16, by paulson
Now also proves monotonicity when in quick_and_dirty mode.
2000-06-15, by berghofe
tidied
2000-06-14, by paulson
full_rename_numerals -> rename_numerals; tidied
2000-06-14, by paulson
a big tidy-up
2000-06-14, by paulson
installing the cancel_numerals and combine_numerals simprocs
2000-06-14, by paulson
tuned tappl syntax;
2000-06-14, by wenzelm
theorems [cases type: bool] = case_split;
2000-06-14, by wenzelm
full_rename_numerals -> rename_numerals; tidied
2000-06-14, by paulson
tidied a proof using new lemmas for signs of products
2000-06-14, by paulson
new lemmas for signs of products
2000-06-14, by paulson
new default simprules for m*n = 0
2000-06-14, by paulson
tuned;
2000-06-13, by wenzelm
rename @case to _case_syntax (improves on low-level errors);
2000-06-13, by wenzelm
updated;
2000-06-13, by wenzelm
qed_spec_mp: strip_shyps_warning;
2000-06-13, by wenzelm
* browser info session directories are now self-contained (may be put
2000-06-09, by wenzelm
prf_open/close;
2000-06-08, by wenzelm
replacing 0hr by (0::hypreal)
2000-06-07, by paulson
minor tuning for pdf documents
2000-06-07, by kleing
tidied
2000-06-07, by paulson
provide TAGS file for Isabelle sources;
2000-06-07, by wenzelm
string syntax: allow \\ \" \\n only;
2000-06-07, by wenzelm
update_thy_only: setmp Thm.trace_simp false;
2000-06-07, by wenzelm
renamed mktags to maketags;
2000-06-07, by wenzelm
generate TAGS file for Isabelle sources;
2000-06-07, by wenzelm
Removed cp / mkdir commands for graph browser files.
2000-06-07, by berghofe
Exported system_command.
2000-06-07, by berghofe
Removed codebase attribute from applet_pages.
2000-06-07, by berghofe
Reorganized graph stuff.
2000-06-07, by berghofe
First round of changes, towards installation of simprocs
2000-06-07, by paulson
Real/simproc.ML now removed
2000-06-07, by paulson
tidied
2000-06-07, by paulson
pair split: proper names of params;
2000-06-06, by wenzelm
added rule_params;
2000-06-06, by wenzelm
session.tex: nsert blank lines in order to guarantee new paragraphs
2000-06-06, by wenzelm
opt_mixfix', opt_infix';
2000-06-04, by wenzelm
do not setmp Library.timing;
2000-06-04, by wenzelm
removed explicit terminator (";");
2000-06-04, by wenzelm
removed method;
2000-06-04, by wenzelm
improved terminator msg;
2000-06-04, by wenzelm
block commands: marginal comment;
2000-06-03, by wenzelm
fixed Thm.eq_thm: use Sign.joinable;
2000-06-03, by wenzelm
'next', '{', '}': comment;
2000-06-03, by wenzelm
removed brace aliases;
2000-06-03, by wenzelm
added HOL/Prolog
2000-06-02, by oheimb
The Allocator Implementation (not yet working)
2000-06-02, by paulson
lots of new results about sublist, bag_of
2000-06-02, by paulson
new theorem increasing_constant
2000-06-02, by paulson
new constant bag_of
2000-06-02, by paulson
added eta_contract_eq, also to simpset
2000-06-02, by oheimb
added rtranclD, tranclD, irrefl_trancl_rD
2000-06-02, by oheimb
new theorems Always_Constrains_weaken and Always_Compl_Un_eq
2000-06-02, by paulson
added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq
2000-06-02, by oheimb
new parent MultisetOrder and new results about multiset unions
2000-06-02, by paulson
added map_of_mapk_SomeI and weak_map_of_SomeI
2000-06-02, by oheimb
Many new theorems about multisets and their ordering, including basic
2000-06-02, by paulson
*** empty log message ***
2000-06-02, by nipkow
added HOL/Prolog
2000-06-02, by oheimb
simplified the proof of nth_upt
2000-06-01, by paulson
Updated files to remove 0r and 1r from theorems in descendant theories
2000-06-01, by fleuriot
switched to Isar proofs
2000-05-31, by kleing
Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to
2000-05-31, by wenzelm
Toplevel.no_timing;
2000-05-31, by wenzelm
transfer now automatic;
2000-05-31, by wenzelm
removed 'transfer' att (is now automatic);
2000-05-31, by wenzelm
get_thm(s): automatic transfer;
2000-05-31, by wenzelm
tuned tactic emulation;
2000-05-31, by wenzelm
removed 'transfer' att;
2000-05-31, by wenzelm
moved some theorems to Finite.ML
2000-05-31, by paulson
added new proofs and simplified an old one
2000-05-31, by paulson
new theorems (some from Multiset)
2000-05-31, by paulson
the is now defined using primrec, avoiding explicit use of arbitrary.
2000-05-30, by berghofe
cleaned up;
2000-05-30, by wenzelm
global timing flag;
2000-05-30, by wenzelm
fixed comment;
2000-05-30, by wenzelm
renamed trace/stat_norm_ast to trace/stat_ast;
2000-05-30, by wenzelm
renamed Syntax.trace_norm_ast to Syntax.trace_ast;
2000-05-30, by wenzelm
proof_timing replaced by global timing;
2000-05-30, by wenzelm
* ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
2000-05-30, by wenzelm
Collect_neg_eq;
2000-05-28, by wenzelm
\newcommand{\indexisarcase};
2000-05-28, by wenzelm
case 'antecedent';
2000-05-28, by wenzelm
write major keywords;
2000-05-26, by wenzelm
sublist and some lemmas about it
2000-05-26, by paulson
a more robust proof
2000-05-26, by paulson
fixed the dependences
2000-05-26, by paulson
tidied
2000-05-26, by paulson
restored some of the lessThans
2000-05-26, by paulson
addss -> force_tac
2000-05-26, by paulson
named the primrec clauses of upt
2000-05-26, by paulson
renamed upt_Suc, since that name is needed for its primrec rule
2000-05-26, by paulson
new setsum results
2000-05-26, by paulson
tuned case_tac;
2000-05-26, by wenzelm
updated acknowledgements
2000-05-26, by paulson
fixed the documentation of goalw_cterm and prove_goalw_cterm
2000-05-26, by paulson
res_inst_tac, etc., no longer print the "dest_state" message when the selected
2000-05-25, by paulson
setsum replaces sum_below
2000-05-25, by paulson
moved mostly to HOL/SetInterval.ML and UNITY/UNITY.ML
2000-05-25, by paulson
sum_below moved here from Arith
2000-05-25, by paulson
improved error msgs, listing variable names
2000-05-25, by paulson
better indentation; declared function "null"
2000-05-25, by paulson
new default rules
2000-05-25, by paulson
deleted sum_below: no need for it with setsum and lessThan
2000-05-25, by paulson
documented permute_prems
2000-05-25, by paulson
better indentation
2000-05-25, by paulson
overloading of 0
2000-05-25, by paulson
added "done" proof;
2000-05-24, by wenzelm
proper token_translation for latex mode;
2000-05-24, by wenzelm
some lemmas about plus_ac0
2000-05-24, by paulson
setsum is now overloaded on plus_ac0; lemmas about lessThan, etc.
2000-05-24, by paulson
setsum is now overloaded on plus_ac0
2000-05-24, by paulson
installing plus_ac0 for nat
2000-05-24, by paulson
we must not require SetInterval this early
2000-05-24, by paulson
installing the plus_ac0 axclass
2000-05-24, by paulson
Adding SetInterval, deleting UNITY/LessThan
2000-05-24, by paulson
added parent
2000-05-24, by paulson
facts about lessThan, etc., mostly from UNITY/LessThan
2000-05-24, by paulson
installing the plus_ac0 simprules
2000-05-24, by paulson
rewrote a very long proof (Key_analz_image_Key) because it had stopped working
2000-05-24, by paulson
overloaded 0
2000-05-24, by paulson
tidying for overloaded 0, setsum, etc.
2000-05-24, by paulson
installing plus_ac0 for multisets
2000-05-24, by paulson
replacing "below" by "lessThan"
2000-05-24, by paulson
installing plus_ac0 for int
2000-05-24, by paulson
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
2000-05-24, by paulson
tuned;
2000-05-24, by wenzelm
"done" command;
2000-05-24, by wenzelm
fixed index;
2000-05-24, by wenzelm
restored NatSum.thy
2000-05-24, by paulson
now 0 is overloaded
2000-05-23, by paulson
added type constraint ::nat because 0 is now overloaded
2000-05-23, by paulson
IntRingDefs is now redundant
2000-05-23, by paulson
new type class "zero" so that 0 can be overloaded
2000-05-23, by paulson
finally sum_below is overloaded properly
2000-05-23, by paulson
Multisets have a zero: the empty multiset
2000-05-23, by paulson
defining 0::int to be (int 0)
2000-05-23, by paulson
Now that 0 is overloaded, constant "zero" and its type class "zero" are
2000-05-23, by paulson
added type constraint ::nat because 0 is now overloaded
2000-05-23, by paulson
theory file NatSum.thy no longer needed
2000-05-23, by paulson
theory file NatSum.thy no longer needed
2000-05-23, by paulson
Sums of geometric series
2000-05-23, by paulson
use of AllocBase
2000-05-23, by paulson
removal of lessThan; use of AllocBase
2000-05-23, by paulson
declared sum_below
2000-05-23, by paulson
new files for the Allocator
2000-05-23, by paulson
eta-expanded to handle value polymorphism
2000-05-23, by paulson
improved warning messages;
2000-05-23, by wenzelm
SetInterval
2000-05-23, by nipkow
Added SetInterval
2000-05-23, by nipkow
new Isar version of HOL-AxClasses-Tutorial;
2000-05-22, by wenzelm
tuned;
2000-05-22, by wenzelm
* Pure: changed syntax of local blocks from {{ }} to { };
2000-05-22, by wenzelm
new Isar version;
2000-05-22, by wenzelm
tidied and made to work with AddSIs [psubsetI]
2000-05-22, by paulson
further tidying
2000-05-22, by paulson
loading the new theory MultisetOrder
2000-05-22, by paulson
multisets are partially ordered
2000-05-22, by paulson
Proving that multisets are partially ordered
2000-05-22, by paulson
Proving that multisets are partially ordered
2000-05-22, by paulson
psubsetI is a safe rule
2000-05-22, by paulson
new file Induct/MultisetOrder.thy
2000-05-22, by paulson
fold_commute, fold_nest_Un_Int, setsum_Un and other new results
2000-05-22, by paulson
tuned;
2000-05-22, by wenzelm
added NatClass;
2000-05-22, by wenzelm
show_consts no longer requires show_types;
2000-05-22, by wenzelm
tuned;
2000-05-22, by wenzelm
tuned;
2000-05-22, by wenzelm
obsolete;
2000-05-22, by wenzelm
added notes;
2000-05-21, by wenzelm
new Isar version;
2000-05-21, by wenzelm
replaced {{ }} by { };
2000-05-21, by wenzelm
cite isabelle-axclass;
2000-05-21, by wenzelm
improved \BG, \EN;
2000-05-21, by wenzelm
removed is_type_abbr;
2000-05-21, by wenzelm
removed is_type_abbr;
2000-05-21, by wenzelm
adapted to inner syntax of sorts;
2000-05-21, by wenzelm
replaced {{ }} by { };
2000-05-21, by wenzelm
added sort_of_term;
2000-05-21, by wenzelm
added read_sort;
2000-05-21, by wenzelm
*** empty log message ***
2000-05-21, by wenzelm
new stuff;
2000-05-21, by wenzelm
\urlstyle{rm};
2000-05-21, by wenzelm
snapshot of new Isar'ized version;
2000-05-21, by wenzelm
added lemma.
2000-05-20, by nipkow
fixed link
2000-05-20, by nipkow
* HOL/ML: even fewer consts are declared as global (see theories Ord,
2000-05-18, by wenzelm
print_state: flag for proof only;
2000-05-18, by wenzelm
hide: check declared;
2000-05-18, by wenzelm
added disable_pr, enable_pr;
2000-05-18, by wenzelm
'pr' now prints actual proof states only;
2000-05-18, by wenzelm
fewer consts declared as global;
2000-05-18, by wenzelm
'apply' consumes facts;
2000-05-18, by wenzelm
Proof General -- if present make this the default;
2000-05-17, by wenzelm
export generic_simp_tac;
2000-05-17, by wenzelm
changed to cope with the rewriting of #2+n to Suc(Suc n)
2000-05-16, by paulson
new policy to simplify the use of numerals:
2000-05-16, by paulson
reverted to old proof of dominoes_tile_row, given new treatment of #2+...
2000-05-16, by paulson
Replaced some definitions involving epsilon by more readable primrec
2000-05-15, by berghofe
alist_rec and assoc are now defined using primrec and thus no longer
2000-05-15, by berghofe
Removed unnecessary primrec equations of hd and last involving arbitrary.
2000-05-15, by berghofe
collected three proofs into rename_client_map_tac
2000-05-15, by paulson
added the dummy theory Integ/NatSimprocs.thy
2000-05-15, by paulson
updated
2000-05-12, by paulson
new simprules needed because of new subtraction rewriting
2000-05-12, by paulson
nat_diff_split' now called nat_diff_split
2000-05-12, by paulson
deleted a lot of obsolete arithmetic lemmas
2000-05-12, by paulson
tidied
2000-05-12, by paulson
new simprules for nat_case and nat_rec
2000-05-12, by paulson
tidying, especially to remove zcompare_rls from proofs
2000-05-12, by paulson
a massive tidy-up
2000-05-12, by paulson
NatSimprocs is now a theory, not a file
2000-05-12, by paulson
new theorem one_le_power
2000-05-12, by paulson
tidied
2000-05-12, by paulson
deleted some redundant simprules
2000-05-12, by paulson
new dummy theory; prevents strange errors when loading NatSimprocs.ML
2000-05-12, by paulson
improved name of simproc;
2000-05-12, by wenzelm
fixed theory deps;
2000-05-10, by wenzelm
base on IntArith instead of Int (in order to leave out deleted simproc!);
2000-05-10, by wenzelm
dest_mss: sort procs wrt. names;
2000-05-10, by wenzelm
FAKE_BUILD;
2000-05-10, by wenzelm
polyml;
2000-05-10, by wenzelm
tuned;
2000-05-10, by wenzelm
new default simprule for better compatibility with old setup
2000-05-10, by paulson
tidied
2000-05-10, by paulson
tuned;
2000-05-10, by wenzelm
use proper version of pdfsetup.sty;
2000-05-09, by wenzelm
added semicolons;
2000-05-09, by wenzelm
updated keywords;
2000-05-09, by wenzelm
named "op ^" definitions;
2000-05-09, by wenzelm
improved X-Symbol stuff;
2000-05-09, by wenzelm
more examples
2000-05-09, by paulson
added INSTALL;
2000-05-08, by wenzelm
moved theory Sexp to Induct examples;
2000-05-08, by wenzelm
strip = impI allI allI;
2000-05-08, by wenzelm
replaced rabs by overloaded abs;
2000-05-08, by wenzelm
yet another example
2000-05-08, by paulson
new example
2000-05-08, by paulson
tidied
2000-05-08, by paulson
better simplification of the result of simprocs
2000-05-08, by paulson
moved le_square, proved le_cube
2000-05-08, by paulson
more details
2000-05-08, by paulson
tuned msg;
2000-05-08, by wenzelm
val needs_filtered_use = true;
2000-05-08, by wenzelm
recovered \seealso;
2000-05-08, by wenzelm
improved indexing;
2000-05-08, by wenzelm
\usepackage{makeidx};
2000-05-08, by wenzelm
tuned GARBAGE;
2000-05-08, by wenzelm
improved handling of Isabelle styles (less garbage);
2000-05-08, by wenzelm
updated;
2000-05-08, by wenzelm
updated syntax of simp options: (no_asm) etc.;
2000-05-08, by wenzelm
removed \isabelledefaultstyle (use \isabellestyle instead);
2000-05-08, by wenzelm
always discgarb -c;
2000-05-08, by wenzelm
fixed clash with new 'abs' const;
2000-05-06, by wenzelm
use Sign.simple_read_term;
2000-05-05, by wenzelm
error msg: counting from one (again), in order to be consistent with
2000-05-05, by wenzelm
tuned messages;
2000-05-05, by wenzelm
removed dead code: listof;
2000-05-05, by wenzelm
use Args.colon / Args.parens;
2000-05-05, by wenzelm
adapted to new arithmetic simprocs;
2000-05-05, by wenzelm
added scan_to_id (used to be in Pure/section_utils.ML);
2000-05-05, by wenzelm
removed Pure/section_utils.ML;
2000-05-05, by wenzelm
improved syntax of method options (no_asm) etc;
2000-05-05, by wenzelm
removed index2;
2000-05-05, by wenzelm
updated;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
GPLed;
2000-05-05, by wenzelm
added simple_read_term;
2000-05-05, by wenzelm
tuned msg;
2000-05-05, by wenzelm
Added constant abs.
2000-05-05, by nipkow
simprocs now simplify the RHS of their result
2000-05-05, by paulson
new lemmas about binary division
2000-05-05, by paulson
Added AVL
2000-05-05, by nipkow
if_weak_cong should make linear arithmetic faster
2000-05-04, by paulson
a safer way of proving literal equalities
2000-05-04, by paulson
from Suc...Suc to #m
2000-05-04, by paulson
of course it should use Main
2000-05-04, by paulson
new lemmas concerning powers and #mmm
2000-05-04, by paulson
changed 2 to #2
2000-05-04, by paulson
Suc 0 -> 1
2000-05-04, by paulson
card_Pow is no longer a default simprule because it uses unary 2
2000-05-04, by paulson
simprocs
2000-05-04, by paulson
further tidying of integer simprocs
2000-05-04, by paulson
removed obsolete simproc combine_coeff
2000-05-03, by paulson
Installation of CombineNumerals for the integers
2000-05-03, by paulson
removed obsolete simprocs
2000-05-03, by paulson
removed obsolete "evenness" proofs
2000-05-02, by paulson
TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES
2000-05-02, by paulson
modified for new simprocs
2000-05-02, by paulson
now using binary naturals
2000-05-02, by paulson
various bug fixes
2000-05-02, by paulson
Cassini identity is easier to prove using INTEGERS
2000-05-02, by paulson
a more modern proof
2000-05-02, by paulson
now with combine_numerals
2000-05-02, by paulson
combine_numerals replaces both fold_Suc and combine_coeff
2000-05-02, by paulson
new simproc, replacing combine_coeffs and working for nat, int, real
2000-05-02, by paulson
signature change
2000-04-28, by paulson
inserted triviality check
2000-04-28, by paulson
*** empty log message ***
2000-04-25, by nipkow
new, but still slow, proofs using binary numerals
2000-04-23, by paulson
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
2000-04-23, by paulson
number_of now takes a type arg
2000-04-23, by paulson
this change saves 15 seconds
2000-04-23, by paulson
bug fixes to new simprocs
2000-04-23, by paulson
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
2000-04-23, by paulson
removed some duplication, etc.
2000-04-23, by paulson
now uses the new cancel_numerals simproc
2000-04-23, by paulson
Provers/Arith/inverse_fold.ML is already obsolete
2000-04-21, by paulson
cleaner exceptions
2000-04-21, by paulson
now works for coefficients, not just for numerals
2000-04-21, by paulson
new file containing simproc invocations, from NatBin.ML
2000-04-21, by paulson
moved the simproc code to NatSimprocs.ML
2000-04-21, by paulson
Provers/Arith/inverse_fold.ML is already obsolete
2000-04-21, by paulson
new file Integ/NatSimprocs.ML
2000-04-21, by paulson
Provers/Arith/inverse_fold.ML is already obsolete
2000-04-21, by paulson
*** empty log message ***
2000-04-20, by nipkow
*** empty log message ***
2000-04-19, by nipkow
TuturialI;
2000-04-19, by wenzelm
*** empty log message ***
2000-04-19, by nipkow
check_file: keep expanded (!) absolute path;
2000-04-19, by wenzelm
Adding generated files
2000-04-19, by nipkow
*** empty log message ***
2000-04-19, by nipkow
fixed -c default value;
2000-04-19, by wenzelm
Adding generated files.
2000-04-19, by nipkow
I wonder which files i forgot.
2000-04-19, by nipkow
*** empty log message ***
2000-04-19, by nipkow
I wonder if that's all?
2000-04-19, by nipkow
deleted obsolete lemma_not_leI2
2000-04-19, by paulson
removal of less_SucI, le_SucI from default simpset
2000-04-19, by paulson
replaced obsolete diff_right_cancel by diff_diff_eq
2000-04-18, by paulson
added number_of_const: term
2000-04-18, by paulson
tidied
2000-04-18, by paulson
instantiates new simprocs for numerals of type "nat"
2000-04-18, by paulson
new simprocs for numerals of type "nat"
2000-04-18, by paulson
emilimated global names;
2000-04-18, by wenzelm
removed obsolete "simpset" keyword;
2000-04-18, by wenzelm
renamed 'hide' to 'hide_action';
2000-04-18, by wenzelm
fixed theory deps;
2000-04-18, by wenzelm
made SML/NJ happy;
2000-04-17, by wenzelm
made SML/NJ happy;
2000-04-17, by wenzelm
* improved name spaces: ambiguous output is qualified; support for
2000-04-17, by wenzelm
improved output of ambiguous entries;
2000-04-17, by wenzelm
Pretty.chunks;
2000-04-17, by wenzelm
'global' / 'local': comment;
2000-04-17, by wenzelm
name space hide operations;
2000-04-17, by wenzelm
global/local_path: comment;
2000-04-17, by wenzelm
added 'hide';
2000-04-17, by wenzelm
tuned msg;
2000-04-17, by wenzelm
NameSpace.is_qualified;
2000-04-17, by wenzelm
Pretty.chunks;
2000-04-17, by wenzelm
mod to error msg
2000-04-15, by nipkow
next_block: reset_facts;
2000-04-15, by wenzelm
plain ASCII;
2000-04-15, by wenzelm
intrn_arity: reject type abbreviations;
2000-04-14, by wenzelm
added is_type_abbr;
2000-04-14, by wenzelm
\newenvironment{isabellequote};
2000-04-14, by wenzelm
global \isa@parindent, \isa@parskip;
2000-04-14, by wenzelm
use HOLogic.termT;
2000-04-14, by wenzelm
outer syntax: no simps;
2000-04-13, by wenzelm
recdef: no simps;
2000-04-13, by wenzelm
stopped using the obsolete "nat_ind_tac"
2000-04-13, by paulson
added some new iff-lemmas; removed some obsolete thms
2000-04-13, by paulson
tidied
2000-04-13, by paulson
tuned;
2000-04-13, by wenzelm
*** empty log message ***
2000-04-13, by nipkow
Simplifier options;
2000-04-13, by wenzelm
Times -> <*>
2000-04-13, by nipkow
fixed ??/?;
2000-04-13, by wenzelm
fixed index;
2000-04-13, by wenzelm
added simp_options;
2000-04-13, by wenzelm
intro/elim_tac: match only;
2000-04-13, by wenzelm
made mod_less_divisor a simplification rule.
2000-04-13, by nipkow
InductMethod.concls_of;
2000-04-12, by wenzelm
tuned;
2000-04-12, by wenzelm
export concl_of;
2000-04-12, by wenzelm
tuned \isasymlbrace;
2000-04-12, by wenzelm
'insts' syntax;
2000-04-12, by wenzelm
improved 'induct(_tac)' syntax;
2000-04-12, by wenzelm
added 'insert' method;
2000-04-12, by wenzelm
added inst, insts;
2000-04-12, by wenzelm
improved induct_tac;
2000-04-12, by wenzelm
induct stripped: match_tac;
2000-04-12, by wenzelm
Args.name_dummy;
2000-04-12, by wenzelm
fixed 'induct_tac' syntax;
2000-04-12, by wenzelm
handle dir prefix;
2000-04-10, by wenzelm
improved document preparation;
2000-04-10, by wenzelm
fixed comment;
2000-04-08, by wenzelm
added 'ML_command';
2000-04-07, by wenzelm
apply etc.: comments;
2000-04-07, by wenzelm
tuned \isasymlbrace;
2000-04-06, by wenzelm
added \isasymlbrace, \isasymrbrace, \isasymtop;
2000-04-06, by wenzelm
'welcome' made diagnostic;
2000-04-06, by wenzelm
added Isar_examples/NestedDatatype.thy;
2000-04-05, by wenzelm
added NestedDatatype.thy;
2000-04-05, by wenzelm
added NestedDatatype;
2000-04-05, by wenzelm
fixed goal selection;
2000-04-05, by wenzelm
Isar: simplified (more robust) goal selection of proof methods;
2000-04-05, by wenzelm
induct/case_tac emulation: optional rule;
2000-04-05, by wenzelm
HEADGOAL;
2000-04-05, by wenzelm
tuned comment;
2000-04-05, by wenzelm
removed "as" keyword;
2000-04-05, by wenzelm
suppress warning;
2000-04-05, by wenzelm
print_simpset / print_claset command;
2000-04-04, by wenzelm
case_tac / induct_tac: optional rule;
2000-04-04, by wenzelm
case_tac, induct_tac;
2000-04-04, by wenzelm
'let': replaced 'as' by 'and';
2000-04-04, by wenzelm
tuned recover;
2000-04-03, by wenzelm
isapar, isamarkuptext, isamarkuptxt turned into environments;
2000-04-03, by wenzelm
markup_env_command 'text' / 'txt';
2000-04-03, by wenzelm
support markup environments;
2000-04-03, by wenzelm
tuned presentation;
2000-04-01, by wenzelm
proper naming of fib equations;
2000-04-01, by wenzelm
recdef: admit names/atts;
2000-04-01, by wenzelm
isatool document: tuned -c option;
2000-04-01, by wenzelm
recdef: admit name and atts;
2000-04-01, by wenzelm
tuned -c option;
2000-04-01, by wenzelm
recover: observe stopper;
2000-04-01, by wenzelm
presentation ignore stuff: swallow newline;
2000-04-01, by wenzelm
added is_newline;
2000-04-01, by wenzelm
'cd': diag;
2000-04-01, by wenzelm
more robust handling of explicit rules;
2000-04-01, by wenzelm
tuned mixfix syntax;
2000-04-01, by wenzelm
added ProofGeneral.undo;
2000-04-01, by wenzelm
isatool document: check output file (workaround PolyML problem with RC);
2000-04-01, by wenzelm
use cong_add_global att;
2000-03-31, by wenzelm
added cong atts;
2000-03-31, by wenzelm
added cong atts;
2000-03-31, by wenzelm
made SML/XL happy;
2000-03-31, by wenzelm
change_global/local_css move to Provers/clasimp.ML;
2000-03-31, by wenzelm
setup cong_attrib_setup;
2000-03-31, by wenzelm
added change_global/local_css;
2000-03-31, by wenzelm
added 'cong' att;
2000-03-31, by wenzelm
tuned;
2000-03-31, by wenzelm
params: preserve case names;
2000-03-31, by wenzelm
fixed indexing of elim rules;
2000-03-31, by wenzelm
use Attrib.add_del_args;
2000-03-31, by wenzelm
added add_del_args;
2000-03-31, by wenzelm
fixed goal syntax;
2000-03-31, by wenzelm
comments modified
2000-03-31, by nipkow
tuned
2000-03-31, by kleing
included new stanford mirror, mirror links now point to source directly
2000-03-31, by kleing
updated recdef
2000-03-31, by nipkow
tuned;
2000-03-30, by wenzelm
recdef
2000-03-30, by nipkow
If all termination conditions are proved automatically,
2000-03-30, by nipkow
recdef.rules -> recdef.simps
2000-03-30, by nipkow
mod in recdef allows to access the correct simpset via simpset().
2000-03-30, by nipkow
the simplification rules returned from TFL are now paired with the row they
2000-03-30, by nipkow
* Isar/Pure: local results and corresponding term bindings are now
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in results and bindings;
2000-03-30, by wenzelm
added 'moreover' and 'ultimately';
2000-03-30, by wenzelm
added \MOREOVER, \ULTIMATELY;
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in binds and facts;
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in binds and facts;
2000-03-30, by wenzelm
let_bind(_i): polymorphic version;
2000-03-30, by wenzelm
ProofContext.find_free;
2000-03-30, by wenzelm
'tactic': refer to PureIsar structure;
2000-03-30, by wenzelm
?this: support params;
2000-03-30, by wenzelm
support polymorphic Vars;
2000-03-30, by wenzelm
tuned;
2000-03-30, by wenzelm
foldl_term_types: depend on term as well;
2000-03-30, by wenzelm
read_def_cterms: use Sign.read_def_terms;
2000-03-30, by wenzelm
read_def_terms (no certify yet);
2000-03-30, by wenzelm
export update_multi;
2000-03-30, by wenzelm
added tvars_intr_list;
2000-03-30, by wenzelm
*** empty log message ***
2000-03-29, by nipkow
*** empty log message ***
2000-03-29, by nipkow
mods because of weak_case_cong -> removed Action.ML twice
2000-03-28, by nipkow
added weak_case_cong feature
2000-03-28, by nipkow
mods because of weak_case_cong
2000-03-28, by nipkow
fixed railqtoken;
2000-03-28, by wenzelm
-I option;
2000-03-28, by wenzelm
renamed 'hoare_vcg' to 'hoare';
2000-03-27, by wenzelm
tuned;
2000-03-27, by wenzelm
fixed dddot_tr;
2000-03-27, by wenzelm
rail token vs. terminal;
2000-03-27, by wenzelm
fixed term syntax;
2000-03-27, by wenzelm
tail token vs. terminal;
2000-03-27, by wenzelm
fixed \rail@tokenfont (ever used?);
2000-03-27, by wenzelm
added an order-sorted version of quickSort
2000-03-27, by paulson
simplified constant "colored"
2000-03-27, by paulson
added 'ultimately';
2000-03-26, by wenzelm
added WhileRule';
2000-03-26, by wenzelm
made SML/NJ happy;
2000-03-26, by wenzelm
tuned presentation;
2000-03-26, by wenzelm
tuned;
2000-03-26, by wenzelm
ignore_stuff;
2000-03-26, by wenzelm
tuned output;
2000-03-26, by wenzelm
!!!! = cut "Corrupted outer syntax in presentation";
2000-03-26, by wenzelm
added is_begin/end_ignore;
2000-03-26, by wenzelm
tuned targets;
2000-03-26, by wenzelm
tuned;
2000-03-25, by wenzelm
improved (anti)quote_tr(');
2000-03-25, by wenzelm
addsimprocs [record_simproc];
2000-03-25, by wenzelm
tuned antiquote_tr';
2000-03-25, by wenzelm
export updateN;
2000-03-25, by wenzelm
use abstract syntax;
2000-03-24, by wenzelm
plain ASCII;
2000-03-24, by wenzelm
arith method: HEADGOAL;
2000-03-24, by wenzelm
HOL/ex/Multiquote;
2000-03-24, by wenzelm
added HOL/ex/Multiquote.thy;
2000-03-24, by wenzelm
tuned;
2000-03-24, by wenzelm
usedir -D: update styles as well;
2000-03-24, by wenzelm
usedir -D: update styles;
2000-03-24, by wenzelm
improved dump of styles;
2000-03-24, by wenzelm
-o sty;
2000-03-24, by wenzelm
comments
2000-03-24, by nipkow
added 'moreover' command;
2000-03-23, by wenzelm
tuned output;
2000-03-23, by wenzelm
tuned spacing;
2000-03-23, by wenzelm
ex/Antiquote.thy made new-style theory;
2000-03-23, by wenzelm
now exclusively uses rtac/dtac/etac rather than the long forms
2000-03-23, by paulson
restored the MESON examples file HOL/ex/mesontest2.ML
2000-03-23, by paulson
made a proof more robust (did not like Suc_less_eq)
2000-03-22, by paulson
Suc_less_eq now with AddIffs. How could this have been overlooked?
2000-03-22, by paulson
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
2000-03-22, by paulson
made more robust
2000-03-22, by paulson
tidied using new "inst" rule
2000-03-22, by paulson
tidied using new "inst" rule
2000-03-22, by paulson
new meta-rule "inst", a shorthand for read_instantiate_sg
2000-03-22, by paulson
goal_spec: [!];
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned comment;
2000-03-21, by wenzelm
help message;
2000-03-21, by wenzelm
handle general case: params and hyps of thesis;
2000-03-21, by wenzelm
soft_asm_tac: hack to norm goal;
2000-03-21, by wenzelm
proof methods: 'case_tac' / 'induct_tac';
2000-03-20, by wenzelm
tuned degenerate cases / induct;
2000-03-20, by wenzelm
added prove_goalw_cterm;
2000-03-20, by wenzelm
quick_and_dirty moved to Isar/skip_proof.ML;
2000-03-20, by wenzelm
use Args.goal_spec;
2000-03-20, by wenzelm
goal_spec;
2000-03-20, by wenzelm
ALLGOALS_RANGE superceded by Seq.INTERVAL;
2000-03-20, by wenzelm
improved support for emulating tactic scripts;
2000-03-20, by wenzelm
res_inst_tac etc.;
2000-03-20, by wenzelm
goalspec;
2000-03-20, by wenzelm
case_tac, induct_tac;
2000-03-20, by wenzelm
tactic emulation;
2000-03-20, by wenzelm
tidied
2000-03-20, by paulson
the perm_rules variable is no longer needed
2000-03-20, by paulson
tidied
2000-03-20, by paulson
replaced best_tac by force_tac, allowing some arithmetic reasoning
2000-03-20, by paulson
renamed a variable to avoid possible free/bound confusion
2000-03-20, by paulson
a possibly (?) more perspicous simprule in the "simpset" part
2000-03-20, by paulson
now based on "Main", as it should be
2000-03-20, by paulson
deleted unnecessary "simpset" part from recdef
2000-03-20, by paulson
'oops' made proper;
2000-03-18, by wenzelm
intro_classes_tac: REPEAT_ALL_NEW;
2000-03-18, by wenzelm
tuned comments;
2000-03-18, by wenzelm
tuned;
2000-03-18, by wenzelm
obtain;
2000-03-18, by wenzelm
simplified setup;
2000-03-18, by wenzelm
pure methods / atts moved here;
2000-03-18, by wenzelm
tuned;
2000-03-18, by wenzelm
obtain;
2000-03-18, by wenzelm
parskip 0pt;
2000-03-17, by wenzelm
tuned;
2000-03-17, by wenzelm
fixed theory, context typing;
2000-03-17, by wenzelm
tuned;
2000-03-17, by wenzelm
simplified Proof General setup;
2000-03-17, by wenzelm
untag: only name arg;
2000-03-17, by wenzelm
arith: "!" arg;
2000-03-17, by wenzelm
x-symbol;
2000-03-17, by wenzelm
fixed \OBTAIN;
2000-03-17, by wenzelm
fixed dep;
2000-03-17, by wenzelm
arith method: bang arg;
2000-03-17, by wenzelm
\isamarkupheader: \section;
2000-03-17, by wenzelm
generic "kill" command;
2000-03-17, by wenzelm
old_symbol_source: include header;
2000-03-17, by wenzelm
kill: include kill_proof;
2000-03-17, by wenzelm
fixed untag;
2000-03-17, by wenzelm
untag: remove all tags of given name;
2000-03-17, by wenzelm
no begin_goal marker (interferes with "latex" etc. output; useless anyway?)
2000-03-17, by wenzelm
next_block: allow in non-goal blocks as well (experimental);
2000-03-17, by wenzelm
re-ordered the theorems
2000-03-17, by paulson
better error messages, especially for multiple types
2000-03-17, by paulson
Splitter support;
2000-03-16, by wenzelm
added HOL/PreLIst.thy;
2000-03-16, by wenzelm
tuned;
2000-03-16, by wenzelm
do not change parindent/parskip;
2000-03-16, by wenzelm
Isar: splitter support; improved diagnostics;
2000-03-16, by wenzelm
Splitter support;
2000-03-16, by wenzelm
moved "cases" to generic.tex;
2000-03-16, by wenzelm
tuned;
2000-03-16, by wenzelm
Named local contexts (cases);
2000-03-16, by wenzelm
Added setup for primrec theory data.
2000-03-15, by berghofe
get_recdef now returns None instead of raising ERROR.
2000-03-15, by berghofe
Added new theory data slot for primrec equations.
2000-03-15, by berghofe
Now returns theorems with correct names in derivations.
2000-03-15, by berghofe
Eliminated store_clasimp.
2000-03-15, by berghofe
- Fixed bug in prove_casedist_thms (proof failed because of
2000-03-15, by berghofe
less
more
|
(0)
-10000
-3072
+3072
+10000
+30000
tip