Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
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
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip