Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Converted main proof to Isar.
2003-04-28, by berghofe
Converted main proofs to Isar.
2003-04-28, by berghofe
Added "break" flag to allow line breaks within \isa{...}
2003-04-28, by berghofe
Fixed problem in add_elim_realizer (concerning inductive predicates with
2003-04-27, by berghofe
converting more HOL-Auth to new-style theories
2003-04-26, by paulson
converting more HOL-Auth to new-style theories
2003-04-26, by paulson
catches exception DELETE
2003-04-26, by paulson
no need to be nice everywhere
2003-04-25, by kleing
Auth: certified email protocol
2003-04-25, by paulson
Changes required by the certified email protocol
2003-04-25, by paulson
Fixed problem in add_elim_realizer which caused bound variables to
2003-04-23, by berghofe
more documentation
2003-04-23, by kleing
Got rid of the [iff], which was effectively inserting converseD
2003-04-23, by paulson
Tuned realizer for exE rule, to avoid blowup of extracted program.
2003-04-23, by berghofe
elim_vars now handles both Vars and Frees.
2003-04-23, by berghofe
elim_cong now eta-expands proofs on the fly if required.
2003-04-23, by berghofe
Eliminated most occurrences of rule_format attribute.
2003-04-23, by berghofe
header
2003-04-16, by nipkow
Added take/dropWhile thms
2003-04-16, by nipkow
fixed document
2003-04-15, by kleing
added thm"..." due to new Map.thy
2003-04-14, by nipkow
Added thms
2003-04-14, by nipkow
Fixed non-escaped underscore in section headings (document generation should
2003-04-14, by webertj
Map.ML integrated into Map.thy
2003-04-11, by webertj
tidying
2003-04-09, by paulson
Removal of Summation theory
2003-04-09, by paulson
Fixed bug in adjustcoeffeq_wp.
2003-04-08, by berghofe
try_param_tac now precomputes substitution for rule, in order to avoid
2003-04-08, by berghofe
First working version
2003-04-08, by nipkow
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
2003-04-07, by nipkow
use 2 processors on sunbroy1
2003-04-06, by kleing
run on sunbroy1, too
2003-04-06, by kleing
*** empty log message ***
2003-04-06, by nipkow
Map.empty is now a translation
2003-04-05, by nipkow
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
cleanup, mark old (<1994) deleted files as dead
2003-04-05, by kleing
removed since 1994 or earlier
2003-04-05, by kleing
Fixed bug in eta_long.
2003-04-04, by berghofe
type_of_G now applies type substitution before decomposing type.
2003-04-04, by berghofe
Made empty a translation rather than a constant.
2003-04-01, by nipkow
Fixed Coset.thy (proved theorem factorgroup_is_group).
2003-04-01, by ballarin
more comments and tweaks
2003-03-31, by paulson
tidied
2003-03-31, by paulson
Margin for pretty-printing is now a mutable reference.
2003-03-29, by berghofe
Proofs for section 4.5.3
2003-03-26, by paulson
Added show_brackets to settings menu.
2003-03-25, by berghofe
Re-structured some proofs in order to get rid of rule_format attribute.
2003-03-25, by berghofe
New theorems split_div' and mod_div_equality'.
2003-03-25, by berghofe
Presburger arithmetic
2003-03-25, by berghofe
Added examples for Presburger arithmetic.
2003-03-25, by berghofe
Added decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
Added Presburger theory.
2003-03-25, by berghofe
Added hook for presburger arithmetic decision procedure.
2003-03-25, by berghofe
New decision procedure for Presburger arithmetic.
2003-03-25, by berghofe
*** empty log message ***
2003-03-23, by nipkow
More on progress sets
2003-03-21, by paulson
quadratic reciprocity files
2003-03-21, by paulson
Gauss, UNITY, ZF
2003-03-20, by paulson
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
2003-03-20, by paulson
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
2003-03-18, by paulson
toggled show_main_goal
2003-03-18, by nipkow
*** empty log message ***
2003-03-18, by nipkow
just a few mods to a few thms
2003-03-17, by nipkow
More "progress set" material
2003-03-17, by paulson
moved one proof, added another
2003-03-17, by paulson
Bugs fixed and operators finprod and finsum.
2003-03-14, by ballarin
more about list_all2
2003-03-14, by kleing
fix for changes in HOL/Hoare/
2003-03-14, by kleing
Proved the main lemma on progress sets
2003-03-14, by paulson
new UN/INT simprules
2003-03-14, by paulson
split_name no longer uses Sign.string_of_typ to encode types, since
2003-03-13, by berghofe
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
*** empty log message ***
2003-03-11, by nipkow
addsplits / delsplits no longer ignore type of constant.
2003-03-11, by berghofe
First distributed version of Group and Ring theory.
2003-03-10, by ballarin
New theory ProgressSets. Definition of closure sets
2003-03-10, by paulson
spelling
2003-03-10, by paulson
new UNITY examples theory
2003-03-06, by paulson
new logical equivalences
2003-03-06, by paulson
new simprule for int (nat n)
2003-03-06, by paulson
link to devel snapshot
2003-03-06, by kleing
obsolete
2003-03-06, by kleing
new examples theory
2003-03-05, by paulson
get cvs to change modified time for session.tex
2003-03-02, by kleing
typo
2003-03-01, by kleing
added exercises
2003-03-01, by kleing
added Exercises
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
keep a copy of generated files in repository
2003-03-01, by kleing
generate nightly devel snapshot
2003-02-28, by isatest
case distinction on host for makefile flags
2003-02-28, by isatest
Reorganized, moving many results about the integer dvd relation from IntPrimes
2003-02-27, by paulson
restored some deleted lemmas
2003-02-27, by paulson
Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-27, by ballarin
== -> =
2003-02-26, by kleing
zprime_def fixes by Jeremy Avigad
2003-02-26, by paulson
completed proofs for programs consisting of a single assignment
2003-02-26, by paulson
new lemma
2003-02-26, by paulson
some x-symbols and some new lemmas
2003-02-26, by paulson
*** empty log message ***
2003-02-25, by nipkow
added simp_depth_limit
2003-02-25, by nipkow
Documented prf / full_prf commands and antiquotations.
2003-02-25, by berghofe
Undid eta change for UN/INT.
2003-02-25, by nipkow
new inverse image lemmas
2003-02-20, by paulson
minor updates to pre-2002 release
2003-02-20, by paulson
fixed anomalies in the installed classical rules
2003-02-19, by paulson
check maxs in defensive machine
2003-02-18, by kleing
new theory Transformers: Meier-Sanders non-interference theory
2003-02-18, by paulson
Proof of the Schorr-Waite graph marking algorithm.
2003-02-17, by mehta
minor revisions
2003-02-16, by paulson
new theorem Compl_partition2
2003-02-16, by paulson
Product operator added --- preliminary.
2003-02-14, by ballarin
favicon
2003-02-12, by kleing
*** empty log message ***
2003-02-11, by nipkow
*** empty log message ***
2003-02-10, by nipkow
New development of algebra: Groups.
2003-02-10, by ballarin
converting HOL/UNITY to use unconditional fairness
2003-02-08, by paulson
adjusted dom rules
2003-02-08, by nipkow
(*f -> ( *f because of new comments
2003-02-07, by nipkow
Removed (*) because of comments
2003-02-07, by nipkow
Added (* ... *) comments in formulae.
2003-02-07, by nipkow
changed ** to ## to avoid conflict with new comment syntax
2003-02-06, by paulson
more tidying
2003-02-05, by paulson
some x-symbols
2003-02-04, by paulson
New tool for displaying version information.
2003-02-03, by berghofe
Fill in version information in lib/Tools/version.
2003-02-03, by berghofe
Added "print_intros" command.
2003-02-03, by berghofe
Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2003-02-03, by berghofe
Moved find_intros_goal from goals.ML to pure_thy.ML
2003-02-03, by berghofe
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2003-02-03, by berghofe
conversion to new-style theories and tidying
2003-01-31, by paulson
conversion of UNITY theories to new-style
2003-01-30, by paulson
converting more UNITY theories to new-style
2003-01-30, by paulson
Some tuning:
2003-01-29, by berghofe
Added function rev_append.
2003-01-29, by berghofe
Fixed bug in function corr.
2003-01-29, by berghofe
converted more UNITY theories to new-style
2003-01-29, by paulson
*** empty log message ***
2003-01-29, by nipkow
converting UNITY to new-style theories
2003-01-29, by paulson
New example
2003-01-28, by nipkow
pos/neg_mod_sign/bound are now simp rules.
2003-01-28, by nipkow
fixed missing UNITY files
2003-01-27, by kleing
More conversion of UNITY to Isar new-style theories
2003-01-24, by paulson
Partial conversion of UNITY to Isar new-style theories
2003-01-24, by paulson
tidying (by script)
2003-01-23, by paulson
Fixed term order for normal form in rings.
2003-01-23, by ballarin
Added rename_abs attribute for renaming bound variables.
2003-01-17, by berghofe
*** empty log message ***
2003-01-17, by nipkow
more new-style theories
2003-01-15, by paulson
moving "let" from ZF to FOL
2003-01-15, by paulson
auto-update
2003-01-15, by paulson
*** empty log message ***
2003-01-09, by nipkow
New files in Hoare/
2003-01-08, by nipkow
corrected swallowing of newlines after end-of-ignore: rollback
2003-01-08, by oheimb
corrected swallowing of newlines after end-of-ignore (improved)
2003-01-07, by oheimb
new versions of merge-example
2003-01-07, by nipkow
Split Pointers.thy and automated one proof, which caused the runtime to explode
2003-01-06, by nipkow
*** empty log message ***
2003-01-05, by nipkow
*** empty log message ***
2003-01-03, by nipkow
*** empty log message ***
2002-12-30, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-29, by nipkow
*** empty log message ***
2002-12-23, by nipkow
removed some problems with print translations
2002-12-22, by nipkow
added print translations tha avoid eta contraction for important binders.
2002-12-22, by nipkow
*** empty log message ***
2002-12-22, by nipkow
*** empty log message ***
2002-12-20, by nipkow
auto-update
2002-12-19, by paulson
*** empty log message ***
2002-12-18, by nipkow
auto-update
2002-12-17, by paulson
new int induction rules
2002-12-17, by paulson
new material for trace_unify_fail
2002-12-17, by paulson
Added mk_int and mk_list.
2002-12-16, by berghofe
Code generator for datatypes now also generates suitable term_of functions (when
2002-12-16, by berghofe
- Added mode reference variable (may be used to switch on and off specific
2002-12-16, by berghofe
cent/currency: changed from wasysym to textcomp because of PDF problems
2002-12-13, by oheimb
trace_unify_fail
2002-12-13, by paulson
integer induction rules
2002-12-13, by paulson
size_of_proof no longer includes size_of_term
2002-12-13, by berghofe
deleted redundant line
2002-12-13, by paulson
Better treatment of equality in premises of inductive definitions. Less
2002-12-12, by paulson
Fixed error that affected document preperation.
2002-12-12, by ballarin
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
2002-12-11, by ballarin
Added size_of_proof.
2002-12-10, by berghofe
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
2002-12-09, by ballarin
corrected swallowing of newlines after end-of-ignore
2002-12-06, by oheimb
*** empty log message ***
2002-12-06, by nipkow
for dvi target
2002-12-05, by kleing
exercise collection
2002-12-05, by kleing
Incompatibility with SML/NJ fixed.
2002-11-29, by ballarin
added a few lemmas
2002-11-29, by nipkow
Transitivity reasoner renamed to linorder.ML. README updated.
2002-11-28, by ballarin
HOL-Algebra partially ported to Isar.
2002-11-28, by ballarin
prop_of now returns proposition in beta-eta normal form.
2002-11-27, by berghofe
- tuned beta_eta_convert
2002-11-27, by berghofe
Correctness proofs are now modular, too.
2002-11-27, by berghofe
Parameters in definitions are now renamed to avoid clashes with
2002-11-27, by berghofe
default_output now escapes \'s more carefully.
2002-11-27, by berghofe
Added XML parser (useful for parsing PGIP / PGML).
2002-11-27, by berghofe
Added some functions for processing PGIP (thanks to David Aspinall).
2002-11-27, by berghofe
Fixed bug in consts_code section.
2002-11-27, by berghofe
Replaced some blasts by rules.
2002-11-27, by berghofe
Changed format of realizers / correctness proofs.
2002-11-27, by berghofe
renamed a few constants
2002-11-25, by nipkow
*** empty log message ***
2002-11-21, by nipkow
textual tweak
2002-11-20, by paulson
stylistic tweaks
2002-11-19, by paulson
beautification
2002-11-18, by nipkow
Fixed small bug that caused some definitions to be "forgotten".
2002-11-17, by berghofe
beautified "match"
2002-11-16, by kleing
beautified "match"
2002-11-16, by kleing
added zdvd_iff_zmod_eq_0
2002-11-15, by nipkow
Improved function decompose.
2002-11-13, by berghofe
- exported functions etype_of and mk_typ
2002-11-13, by berghofe
Fixed name clash problem in forall_elim_var.
2002-11-13, by berghofe
Added simple_prove_goal_cterm.
2002-11-13, by berghofe
Removed (now unneeded) declarations of realizers for bar induction.
2002-11-13, by berghofe
New package for constructing realizers for introduction and elimination
2002-11-13, by berghofe
- No longer applies norm_hhf_rule
2002-11-13, by berghofe
prove_goal' -> Goal.simple_prove_goal_cterm
2002-11-13, by berghofe
name_of_type now replaces non-identifiers by dummy names.
2002-11-13, by berghofe
Added inductive_realizer.
2002-11-13, by berghofe
Added InductiveRealizer package.
2002-11-13, by berghofe
Transitive closure is now defined inductively as well.
2002-11-13, by berghofe
Hoare.ML -> hoare.ML
2002-11-09, by kleing
Polishing.
2002-11-08, by paulson
generalized wf_on_unit to wf_on_any_0
2002-11-08, by paulson
added raw proof blocks
2002-11-07, by nipkow
small improvements
2002-11-07, by nipkow
added show_main_goal
2002-11-07, by nipkow
Hoare.ML -> hoare.ML
2002-11-06, by nipkow
a new pointer example and some syntactic sugar
2002-11-06, by nipkow
two new Bali files
2002-11-05, by kleing
new operator transrec3
2002-11-05, by paulson
Removed obsolete section about reordering assumptions.
2002-11-04, by berghofe
proof streamlining
2002-11-01, by paulson
tidy
2002-11-01, by paulson
Inserted some extra paragraphs in large proofs to make tex run...
2002-11-01, by schirmer
fixed "latex capacity exceeded"
2002-11-01, by kleing
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
2002-10-31, by schirmer
simpler separation/replacement proofs
2002-10-30, by paulson
modified msg
2002-10-30, by nipkow
added induction thms
2002-10-29, by nipkow
moved fac example
2002-10-28, by nipkow
*** empty log message ***
2002-10-28, by nipkow
conversion ML -> thy
2002-10-28, by nipkow
simplified lemma correct_frames_newref
2002-10-27, by kleing
switched to atbroy51, removed markus from email list
2002-10-26, by isatest
fixed latex output
2002-10-25, by kleing
changes for cleanup in JVM
2002-10-24, by kleing
cleanup, beautified
2002-10-24, by kleing
fixed latex error
2002-10-24, by kleing
ASIN -> SET
2002-10-24, by nipkow
*** empty log message ***
2002-10-23, by streckem
First checkin of compiler
2002-10-23, by streckem
Added compiler
2002-10-23, by streckem
Eta contraction is now switched off when printing extracted program.
2002-10-21, by berghofe
Fixed problem with theorems containing TFrees.
2002-10-21, by berghofe
- reconstruct_proof no longer relies on TypeInfer.infer_types
2002-10-21, by berghofe
Removed Logic.skip_flexpairs.
2002-10-21, by berghofe
Replaced variantlist (quadratic) by gen_names (linear).
2002-10-21, by berghofe
Removed add_env because Vartab.map was too slow for large environments.
2002-10-21, by berghofe
- removed flexpair
2002-10-21, by berghofe
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
2002-10-21, by berghofe
Removed flexpair_def.
2002-10-21, by berghofe
Removed Logic.strip_flexpairs.
2002-10-21, by berghofe
No more explicit manipulation of flex-flex constraints in goals_conv.
2002-10-21, by berghofe
Changed type of Logic.strip_horn.
2002-10-21, by berghofe
Removed obsolete functions dealing with flex-flex constraints.
2002-10-21, by berghofe
Changed handling of flex-flex constraints: now stored in separate
2002-10-21, by berghofe
Now applies standard' to "unfold" theorem (due to flex-flex constraints).
2002-10-21, by berghofe
Changed type of Logic.strip_horn.
2002-10-21, by berghofe
Tidying up. New primitives is_iterates and is_iterates_fm.
2002-10-18, by paulson
Mod due to: Added a few thms about UN/INT/{}/UNIV
2002-10-18, by nipkow
Added a few thms about UN/INT/{}/UNIV
2002-10-18, by nipkow
fixed comments and types
2002-10-17, by paulson
Cosmetic changes suggested by writing the paper. Deleted some
2002-10-17, by paulson
fixing the cut_tac method to work when there are no instantiations and the
2002-10-17, by paulson
alternative syntax
2002-10-15, by kleing
*** empty log message ***
2002-10-14, by nipkow
tidying and reorganization
2002-10-14, by paulson
Ported find_intro/elim to Isar.
2002-10-14, by nipkow
norm_typ -> Envir.norm_type
2002-10-11, by berghofe
*** empty log message ***
2002-10-10, by nipkow
*** empty log message ***
2002-10-10, by nipkow
added failure trace information to pattern unification
2002-10-10, by nipkow
Reimplemented parts of datatype package dealing with datatypes involving
2002-10-10, by berghofe
Added list_all.
2002-10-10, by berghofe
Removed obsolete function "fun_rel_comp".
2002-10-10, by berghofe
Added choice_eq.
2002-10-10, by berghofe
- Added range_ex1_eq
2002-10-10, by berghofe
Removed obsolete function "Funs".
2002-10-10, by berghofe
Added functions Suml and Sumr which are useful for constructing
2002-10-10, by berghofe
Re-organization of Constructible theories
2002-10-09, by paulson
type safety with defensive machine
2002-10-08, by kleing
defensive machine
2002-10-08, by kleing
defensive machine without obj init and jsr
2002-10-08, by kleing
Got rid of rotates because of new simplifier
2002-10-08, by nipkow
take/drop -> splitAt
2002-10-07, by nipkow
Various simplifications of the Constructible theories
2002-10-04, by paulson
Fixed bug involving inductive definitions with equalities in the premises.
2002-10-04, by paulson
Fixed bug involving inductive definitions having equalities in the premises,
2002-10-04, by paulson
Documented new "asm_lr" option for simp.
2002-10-04, by berghofe
added the new elim rule psubsetE
2002-10-03, by paulson
*** empty log message ***
2002-10-03, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-02, by nipkow
*** empty log message ***
2002-10-01, by nipkow
Added some comments on new simplifier.
2002-10-01, by berghofe
Documented new "asm_lr" option for simp.
2002-10-01, by berghofe
Adapted to new simplifier.
2002-10-01, by berghofe
Numerous cosmetic changes, prompted by the new simplifier
2002-10-01, by paulson
Deleted superfluous dest_implies.
2002-10-01, by berghofe
*** empty log message ***
2002-09-30, by nipkow
Adapted to new simplifier.
2002-09-30, by berghofe
Adapted to new simplifier.
2002-09-30, by berghofe
Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
2002-09-30, by berghofe
Added check for axioms with "realizes Null A = A".
2002-09-30, by berghofe
Added function elim_vars.
2002-09-30, by berghofe
Completely reimplemented mutual simplification of premises.
2002-09-30, by berghofe
Removed nRS again because extract_rews now takes care of preserving names.
2002-09-30, by berghofe
Added syntax for "asm_lr" simplifier option.
2002-09-30, by berghofe
- eliminated thin_leading_eqs_tac
2002-09-30, by berghofe
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
2002-09-30, by berghofe
- additional congruence rules for boolean operators
2002-09-30, by berghofe
Adapted to new simplifier.
2002-09-30, by berghofe
Removed nRS again because extract_rews now takes care of preserving names.
2002-09-30, by berghofe
Added elim_vars to preprocessor.
2002-09-30, by berghofe
Fixed problem with induct_conj_curry: variable C should have type prop.
2002-09-30, by berghofe
fixes !!-bound vars in induction statement automatically
2002-09-30, by nipkow
modified induct method
2002-09-30, by nipkow
Proof tidying
2002-09-27, by paulson
Isar experiments, etc.
2002-09-27, by paulson
Tidied. New Pi-theorem.
2002-09-27, by paulson
new Ring example
2002-09-27, by paulson
Isar proof
2002-09-27, by paulson
Modules theory added
2002-09-27, by paulson
New theory GroupTheory/Module.thy of modules
2002-09-27, by paulson
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
2002-09-26, by paulson
GroupTheory and FuncSet
2002-09-26, by paulson
new theory for Pi-sets, restrict, etc.
2002-09-26, by paulson
Converted Fun to Isar style.
2002-09-26, by paulson
new document directory for GroupTheory
2002-09-26, by paulson
converted to Isar and using new "implicit structures" instead of Sigma, etc
2002-09-26, by paulson
*** empty log message ***
2002-09-25, by nipkow
*** empty log message ***
2002-09-25, by nipkow
*** empty log message ***
2002-09-25, by nipkow
Int.thy -> int.thy
2002-09-25, by nipkow
became int.ML
2002-09-25, by nipkow
conversion to Isar
2002-09-25, by nipkow
converted to Isar
2002-09-25, by nipkow
added nat_split
2002-09-25, by nipkow
converted to Isar script
2002-09-21, by paulson
shortened a proof
2002-09-20, by paulson
got rid of deepen_tac
2002-09-20, by paulson
less use of x-symbols
2002-09-20, by paulson
*** empty log message ***
2002-09-19, by nipkow
drule: added nRS
2002-09-19, by nipkow
preserve names of rewrite rules when transforming them
2002-09-19, by nipkow
comments + usage
2002-09-18, by kleing
Streamlined proofs of instances of Separation
2002-09-11, by paulson
Bound variable preservation in Collect_cong
2002-09-11, by paulson
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-09-10, by paulson
tweaks
2002-09-10, by paulson
*** empty log message ***
2002-09-09, by nipkow
bug in counter example finder
2002-09-09, by nipkow
conversion of ZF/Integ/{Int,Bin} to Isar scripts
2002-09-07, by paulson
added checking so that (rename_tac "x y") is rejected, since
2002-09-05, by paulson
tidied
2002-09-03, by paulson
deleted redundant material (quasiformula, ...) and rationalized
2002-09-03, by paulson
fixed the typesetting
2002-09-03, by paulson
*** empty log message ***
2002-09-03, by nipkow
Added missing rewrite rule and some arith examples
2002-09-02, by paulson
order_less_irrefl: [simp] -> [iff]
2002-09-02, by nipkow
*** empty log message ***
2002-09-01, by nipkow
converted Hyperreal/Zorn to Isar format and moved to Library
2002-08-31, by paulson
removal of blast.overloaded
2002-08-30, by paulson
updated;
2002-08-29, by wenzelm
*** empty log message ***
2002-08-29, by wenzelm
tuned;
2002-08-29, by wenzelm
fixed a name clash
2002-08-29, by paulson
improved tell_thm_deps;
2002-08-28, by wenzelm
various new lemmas for Constructible
2002-08-28, by paulson
completion of the consistency proof for AC
2002-08-28, by paulson
thms_containing: allow "_" in specification;
2002-08-27, by wenzelm
*** empty log message ***
2002-08-27, by wenzelm
* Pure: disallow duplicate fact bindings within new-style theory files;
2002-08-27, by wenzelm
disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
2002-08-27, by wenzelm
tuned;
2002-08-27, by wenzelm
avoid duplicate fact bindings;
2002-08-27, by wenzelm
removed IsarTut;
2002-08-27, by wenzelm
*** empty log message ***
2002-08-27, by wenzelm
avoid duplicate fact bindings;
2002-08-27, by wenzelm
check_file: disallow current dir (typically "");
2002-08-27, by wenzelm
simplified results;
2002-08-27, by wenzelm
simplified results;
2002-08-27, by wenzelm
Thm.proof_of;
2002-08-27, by wenzelm
check_goal: produce error instead of warning;
2002-08-27, by wenzelm
added proof_of;
2002-08-27, by wenzelm
thms/axms_of_proof: proper handling of MinProof;
2002-08-27, by wenzelm
result dependency output;
2002-08-27, by wenzelm
dup_elim: improved error reporting;
2002-08-27, by wenzelm
*** empty log message ***
2002-08-27, by wenzelm
avoid duplicate fact bindings;
2002-08-27, by wenzelm
* Isar: preview of problems to finish 'show' now produce an error
2002-08-27, by wenzelm
conversion of ZF/IntDiv to Isar script
2002-08-24, by paulson
conversion of ZF/IntDiv to Isar script
2002-08-24, by paulson
*** empty log message ***
2002-08-23, by nipkow
*** empty log message ***
2002-08-23, by nipkow
Added div+mod cancelling simproc
2002-08-23, by nipkow
for cancelling div + mod.
2002-08-23, by nipkow
updated to use locales (still some rough edges);
2002-08-22, by wenzelm
tweaked
2002-08-22, by paulson
tweaks
2002-08-21, by paulson
tweaks and new lemmas
2002-08-21, by paulson
new proof needed now
2002-08-21, by paulson
proof can be shortened now
2002-08-21, by paulson
new lemmas
2002-08-21, by paulson
Frederic Blanqui's new "guard" examples
2002-08-21, by paulson
tidying of Isar scripts
2002-08-17, by paulson
Various tweaks of the presentation
2002-08-16, by paulson
Relativized right up to L satisfies V=L!
2002-08-16, by paulson
Tidying up
2002-08-16, by paulson
Relativization and absoluteness for DPow!!
2002-08-15, by paulson
Finished absoluteness of "satisfies"!!
2002-08-14, by paulson
arith_tac should not produce counter example
2002-08-13, by nipkow
*** empty log message ***
2002-08-13, by nipkow
Counter example generation mods.
2002-08-13, by nipkow
Added counter example generation.
2002-08-13, by nipkow
*** empty log message ***
2002-08-13, by nipkow
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
2002-08-13, by paulson
more robust printing of numerals;
2002-08-13, by wenzelm
new file Constructible/Satisfies_absolute.thy
2002-08-13, by paulson
Lots of new results concerning recursive datatypes, towards absoluteness of
2002-08-12, by paulson
*** empty log message ***
2002-08-12, by nipkow
*** empty log message ***
2002-08-12, by nipkow
Added Mi and Max on sets, hid Min and Pls on numerals.
2002-08-12, by nipkow
*** empty log message ***
2002-08-09, by nipkow
transform_error: pass through Interrupt;
2002-08-08, by wenzelm
tuned;
2002-08-08, by wenzelm
exception SIMPROC_FAIL: solid error reporting of simprocs;
2002-08-08, by wenzelm
tuned prove_conv (error reporting done within meta_simplifier.ML);
2002-08-08, by wenzelm
adhoc_freeze_vars;
2002-08-08, by wenzelm
proper instantiation of mk_left_commute;
2002-08-08, by wenzelm
converted;
2002-08-08, by wenzelm
tuned deps;
2002-08-08, by wenzelm
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-08, by wenzelm
Tactic.prove, Tactic.prove_standard;
2002-08-08, by wenzelm
* Pure: improved error reporting of simprocs;
2002-08-08, by wenzelm
tuned;
2002-08-07, by wenzelm
mk_left_commute: proper instantiation avoids expensive unification;
2002-08-07, by wenzelm
tuned;
2002-08-07, by wenzelm
Simplifier.simproc(_i);
2002-08-07, by wenzelm
Added time example at the end.
2002-08-07, by nipkow
section on "Rule declarations and methods";
2002-08-07, by wenzelm
Removed (now unneeded) declaration of realizer for induction on datatype b.
2002-08-07, by berghofe
Removed (now unneeded) declarations of realizers for induction on lists and letters.
2002-08-07, by berghofe
Added file Tools/datatype_realizer.ML
2002-08-07, by berghofe
Removed (now unneeded) declaration of realizers for induction on natural numbers.
2002-08-07, by berghofe
Module for defining realizers for induction and case analysis theorems
2002-08-07, by berghofe
Added calls to add_dt_realizers.
2002-08-07, by berghofe
Exported function make_tnames.
2002-08-07, by berghofe
Fixed two bugs
2002-08-07, by nipkow
* Provers: Simplifier.simproc(_i) now provide sane interface for
2002-08-06, by wenzelm
sane interface for simprocs;
2002-08-06, by wenzelm
fixed intern_skolem: disallow internal names (why didn't anybody notice?!?);
2002-08-06, by wenzelm
predefined locales "var" and "struct" (useful for sharing parameters);
2002-08-06, by wenzelm
* Pure: predefined locales "var" and "struct" are useful for sharing
2002-08-06, by wenzelm
protect simplifier operation against spurious exceptions from simprocs;
2002-08-05, by wenzelm
tuned;
2002-08-05, by wenzelm
special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);
2002-08-05, by wenzelm
Removed theory NatDef.
2002-08-05, by berghofe
Replaced nat_ind_tac by induct_tac.
2002-08-05, by berghofe
Removed proof of Suc_le_D (already proved in Nat.thy).
2002-08-05, by berghofe
Removed reference to theory NatDef.
2002-08-05, by berghofe
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip