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.
new rule rev_bexI
1998-12-02, by paulson
new theorems Domain_Union, Range_Union
1998-12-02, by paulson
removed duplicate contrapos;
1998-12-01, by wenzelm
enum: !!! after seperator;
1998-12-01, by wenzelm
excursion: ERROR_MESSAGE;
1998-12-01, by wenzelm
qed: kind_name (again);
1998-12-01, by wenzelm
show_tags flag;
1998-12-01, by wenzelm
new theorem INT_Un
1998-12-01, by paulson
better version of Image_diag
1998-12-01, by paulson
tactical CHANGED now uses alpha-eta conversion, not alpha conversion
1998-11-30, by paulson
Renamed subset_Sigma_llist to subset_Times_llist
1998-11-30, by paulson
new theorems about diag
1998-11-30, by paulson
fixed declatation of patterns and skolem;
1998-11-29, by wenzelm
tuned print_state;
1998-11-29, by wenzelm
tuned welcome msg;
1998-11-29, by wenzelm
added restart;
1998-11-29, by wenzelm
added exception RESTART;
1998-11-29, by wenzelm
proof_general_trans (experimental);
1998-11-29, by wenzelm
replaced wakeup by decorate_prompt_fn;
1998-11-29, by wenzelm
eliminated "Trying to recover ..." msg;
1998-11-29, by wenzelm
added oct_char;
1998-11-29, by wenzelm
method brute_force = ALLGOALS force_tac;
1998-11-29, by wenzelm
*** empty log message ***
1998-11-27, by nipkow
At last: linear arithmetic for nat!
1998-11-27, by nipkow
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
1998-11-27, by nipkow
fixed a link
1998-11-27, by paulson
added Real/Hyperreal
1998-11-27, by paulson
Addition of Hyperreal theories Zorn and Filter
1998-11-27, by paulson
moved diag (diagonal relation) from Univ to Relation
1998-11-27, by paulson
tidied up list definitions, using type 'a option instead of
1998-11-26, by paulson
tuning to assimiliate it with PhD;
1998-11-26, by mueller
Added a general refutation tactic which works by putting things into nnf first.
1998-11-26, by nipkow
Added filter_prems_tac
1998-11-26, by nipkow
removed prs / prs_fn;
1998-11-25, by wenzelm
guarantees laws
1998-11-25, by paulson
simplified ensures_UNIV
1998-11-25, by paulson
new thms for invariant
1998-11-25, by paulson
new theorem program_equalityE
1998-11-25, by paulson
renamed vars
1998-11-25, by paulson
image_id in simpset
1998-11-25, by paulson
removed prs / prs_fn (broken, because it did not include \n in its
1998-11-25, by wenzelm
eliminated ISABELLE_INTERFACE_OPTIONS;
1998-11-25, by wenzelm
improved comment;
1998-11-25, by wenzelm
replaced prs by std_output;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
replaced prs by std_output / writeln;
1998-11-25, by wenzelm
comment parser;
1998-11-25, by wenzelm
add_text, add_chapter etc.: dummy;
1998-11-25, by wenzelm
chapter etc. headings;
1998-11-25, by wenzelm
tuned space;
1998-11-25, by wenzelm
replaced prs by writeln;
1998-11-25, by wenzelm
removed redirect_to_latex stuff;
1998-11-25, by wenzelm
Isar.main();
1998-11-24, by wenzelm
setup Blast.setup;
1998-11-24, by wenzelm
added commands;
1998-11-24, by wenzelm
added isar.ML;
1998-11-24, by wenzelm
Isabelle/Isar main interface.
1998-11-24, by wenzelm
fixed prefix_lines: *separate* by \n;
1998-11-24, by wenzelm
added Isar/isar.ML;
1998-11-24, by wenzelm
fixed links
1998-11-23, by paulson
print_state hook, obeys Goals.current_goals_markers by default;
1998-11-21, by wenzelm
print_state: use begin_goal from Goals.current_goals_markers;
1998-11-21, by wenzelm
added undos, redos;
1998-11-21, by wenzelm
tty: issue wakeup;
1998-11-21, by wenzelm
std_output, prefix_lines;
1998-11-21, by wenzelm
better miniscoping rules: the premise C~={} is not good
1998-11-20, by paulson
fixed method syntax;
1998-11-19, by wenzelm
break: exhibit state stack;
1998-11-19, by wenzelm
match_bind: 'as' patterns;
1998-11-19, by wenzelm
let: 'as' patterns;
1998-11-19, by wenzelm
match_bind(_i): 'as' patterns;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
term_pat vs. prop_pat;
1998-11-19, by wenzelm
no warning for "it" theorems;
1998-11-19, by wenzelm
tidied
1998-11-18, by paulson
Finally removing "Compl" from HOL
1998-11-18, by paulson
exn_message FAIL;
1998-11-18, by wenzelm
blast: cla_method';
1998-11-18, by wenzelm
export simp_modifiers;
1998-11-18, by wenzelm
expoer cla_method('), cla_modifiers;
1998-11-18, by wenzelm
method setup;
1998-11-18, by wenzelm
tuned comments;
1998-11-18, by wenzelm
'prop', 'term', 'typ';
1998-11-18, by wenzelm
load;
1998-11-18, by wenzelm
export exn_message;
1998-11-18, by wenzelm
removed trace;
1998-11-18, by wenzelm
BREAK: include state;
1998-11-17, by wenzelm
have_tthms;
1998-11-17, by wenzelm
PureThy.default_name;
1998-11-17, by wenzelm
generalized (opt_)thm_name;
1998-11-17, by wenzelm
exception METHOD_FAIL;
1998-11-17, by wenzelm
added have_theorems, have_lemmas, have_facts;
1998-11-17, by wenzelm
added 'theorems', 'lemmas', 'note';
1998-11-17, by wenzelm
break: exhibit state;
1998-11-17, by wenzelm
exception ATTRIB_FAIL;
1998-11-17, by wenzelm
removed trace;
1998-11-17, by wenzelm
Symbol.space;
1998-11-17, by wenzelm
space;
1998-11-17, by wenzelm
val spc: int -> T;
1998-11-17, by wenzelm
added default_name;
1998-11-17, by wenzelm
Drule.rev_triv_goal;
1998-11-17, by wenzelm
Theory.apply replaced by Library.apply;
1998-11-17, by wenzelm
val apply: ('a -> 'a) list -> 'a -> 'a;
1998-11-17, by wenzelm
export vars_of and friends;
1998-11-17, by wenzelm
Pretty.spc;
1998-11-17, by wenzelm
added pretty_tthms, print_tthms;
1998-11-17, by wenzelm
new theory UNITY/PPROD
1998-11-17, by paulson
new theory PPROD
1998-11-16, by paulson
a faster proof
1998-11-16, by paulson
removed genelim.ML;
1998-11-16, by wenzelm
thm, thms;
1998-11-16, by wenzelm
added print_thm;
1998-11-16, by wenzelm
made SML/NJ happy;
1998-11-16, by wenzelm
added oo, ooo (*concatenation: 2 and 3 args*);
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.tthms_of;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Classical.setup, attrib_setup;
1998-11-16, by wenzelm
attrib_setup: rulify;
1998-11-16, by wenzelm
attrib_setup;
1998-11-16, by wenzelm
all modifiers turned into attributes;
1998-11-16, by wenzelm
tuned attribute names;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
tuned names;
1998-11-16, by wenzelm
renamed tac / etac to refine / then_refine;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
add print_theorems;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
several args parsers;
1998-11-16, by wenzelm
removed args, args1, thm_xname;
1998-11-16, by wenzelm
replaced is_symid by is_sid;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
renamed init_context to init;
1998-11-16, by wenzelm
structure PureIsar;
1998-11-16, by wenzelm
removed lift_modifier;
1998-11-16, by wenzelm
Attribute.thms_of;
1998-11-16, by wenzelm
Scan.read;
1998-11-16, by wenzelm
added read;
1998-11-16, by wenzelm
tuned usage of read;
1998-11-16, by wenzelm
generalized JN_empty and added reachable_SKIP
1998-11-16, by paulson
removed the reference to mesontest2.ML, itself now deleted
1998-11-16, by paulson
moved some facts about Pi from ex/PiSets to Fun.ML
1998-11-16, by paulson
prefixed op;
1998-11-14, by wenzelm
Theory.copy;
1998-11-14, by wenzelm
val copy: theory -> theory;
1998-11-14, by wenzelm
added unless, first;
1998-11-14, by wenzelm
added read_nat;
1998-11-14, by wenzelm
not needed in distribution
1998-11-13, by paulson
needed tidying desperately
1998-11-13, by paulson
qualified the name "restrict" since Fun.restrict exists too
1998-11-13, by paulson
moved Pi and -> (renamed funcset) to Fun.thy
1998-11-13, by paulson
the type of @evalcn was wrong
1998-11-13, by paulson
moved UNION_o to Fun.ML, since Fun.thy is no longer a parent of equalities
1998-11-13, by paulson
no longer loads Fun so that the Fun proofs can use equalities.thy
1998-11-13, by paulson
the function space operator
1998-11-13, by paulson
New section on advanced datatypes.
1998-11-12, by nipkow
*** empty log message ***
1998-11-12, by nipkow
mesontest2.ML was never needed in the distribution
1998-11-12, by paulson
changed inverse syntax from x-| to i(x)
1998-11-12, by paulson
proved surjI
1998-11-11, by paulson
tidied
1998-11-11, by paulson
Big simplification of proofs.
1998-11-11, by paulson
tiny changes;
1998-11-10, by mueller
changed to a link;
1998-11-10, by mueller
local simpset theory data;
1998-11-09, by wenzelm
local claset theory data;
1998-11-09, by wenzelm
Object logic specific operations.
1998-11-09, by wenzelm
Isar setups;
1998-11-09, by wenzelm
added metacuts_tac;
1998-11-09, by wenzelm
removed local_theory;
1998-11-09, by wenzelm
exnMessage Interrupt;
1998-11-09, by wenzelm
added lift_modifier, rule;
1998-11-09, by wenzelm
added Isar;
1998-11-09, by wenzelm
added Isar/;
1998-11-09, by wenzelm
Pure outer syntax.
1998-11-09, by wenzelm
Non-logical toplevel commands.
1998-11-09, by wenzelm
Derived theory operations.
1998-11-09, by wenzelm
The global Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
The Isabelle/Isar toplevel.
1998-11-09, by wenzelm
Histories of proof states, with undo / redo and prev / back.
1998-11-09, by wenzelm
Generic parsers for Isabelle/Isar outer syntax.
1998-11-09, by wenzelm
Outer lexical syntax for Isabelle/Isar.
1998-11-09, by wenzelm
Proof methods.
1998-11-09, by wenzelm
Symbolic theorem attributes.
1998-11-09, by wenzelm
Concrete argument syntax (for attributes, methods etc.).
1998-11-09, by wenzelm
Type-safe interface for proof context data.
1998-11-09, by wenzelm
Proof states and methods.
1998-11-09, by wenzelm
Proof context information.
1998-11-09, by wenzelm
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
1998-11-09, by wenzelm
Check release name and date in NEWS!
1998-11-09, by wenzelm
smart interrupt handler;
1998-11-09, by wenzelm
option -I: startup Isar interaction mode;
1998-11-09, by wenzelm
isabelle -I;
1998-11-09, by wenzelm
fake interrupt handler;
1998-11-09, by wenzelm
simple interrupt_handler;
1998-11-09, by wenzelm
new Domain/Range rules
1998-11-09, by paulson
new TIMES/Sigma rules
1998-11-09, by paulson
removed obsolete comment and "open" declaration
1998-11-09, by paulson
"Subscribe" link
1998-11-06, by paulson
spell check;
1998-11-06, by wenzelm
tuned;
1998-11-06, by wenzelm
added mailing list, removed mirrors;
1998-11-06, by mueller
Revising the Client proof as suggested by Michel Charpentier. New lemmas
1998-11-06, by paulson
made more generic;
1998-11-05, by mueller
Shortened names and added new thm.
1998-11-05, by nipkow
Some streamlining of text.
1998-11-04, by paulson
tuned;
1998-11-03, by wenzelm
tuned width of pics;
1998-11-03, by wenzelm
tuned;
1998-11-03, by wenzelm
oops;
1998-11-02, by wenzelm
tuned pics;
1998-11-02, by wenzelm
made weblint happy;
1998-11-02, by wenzelm
oops;
1998-11-02, by wenzelm
Id;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
tuned;
1998-11-02, by wenzelm
main Isabelle page;
1998-11-02, by wenzelm
New example
1998-11-02, by nipkow
Domain r, Range r replace fst``r, snd``r
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
increased precedence of unary minus from 80 to 100
1998-11-02, by paulson
Charpentier laws
1998-10-31, by paulson
the Increasing operator
1998-10-31, by paulson
no need for int_0
1998-10-31, by paulson
locales now implicitly quantify over free variables
1998-10-31, by paulson
tuned current_goals_markers;
1998-10-30, by wenzelm
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
1998-10-30, by paulson
Explicit (and improved) simprules for binary arithmetic.
1998-10-30, by paulson
*** empty log message ***
1998-10-29, by wenzelm
shyps note for prim. rules;
1998-10-29, by wenzelm
tuned;
1998-10-29, by wenzelm
tuned current_goals_markers semantics to avoid empty lines;
1998-10-29, by wenzelm
tidied
1998-10-29, by paulson
auto update
1998-10-29, by paulson
Some more proofs.
1998-10-28, by nipkow
added nat_diff_split and a few lemmas in Trancl.
1998-10-28, by nipkow
ML_SYSTEM=polyml-3.1;
1998-10-26, by wenzelm
tuned checklist;
Isabelle98-1
1998-10-25, by wenzelm
official release;
1998-10-24, by wenzelm
ML_SYSTEM factory default;
1998-10-24, by wenzelm
*** empty log message ***
1998-10-24, by wenzelm
tuned;
1998-10-24, by wenzelm
records;
1998-10-24, by wenzelm
*** empty log message ***
1998-10-24, by wenzelm
Added theorem bool_induct (for rep_datatype).
1998-10-23, by berghofe
Added theorem unit_induct (for rep_datatype).
1998-10-23, by berghofe
Added theorems True_not_False and False_not_True
1998-10-23, by berghofe
unit and bool are now represented as datatypes.
1998-10-23, by berghofe
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
corrected (and simplified) depth_tac
1998-10-23, by oheimb
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
corrected auto_tac (applications of unsafe wrappers)
1998-10-23, by oheimb
added SOLVE tactical
1998-10-23, by oheimb
tuned;
1998-10-23, by wenzelm
matharray;
1998-10-23, by wenzelm
SYNC: records (draft version);
1998-10-23, by wenzelm
Warns when stack is extended; better decl of print_depth
1998-10-23, by paulson
better checking of "defines" in a locale
1998-10-23, by paulson
better reporting of "Additional hypotheses" in a locale
1998-10-23, by paulson
Now users will never see (int 0)
1998-10-23, by paulson
auto update
1998-10-23, by paulson
updated as requested by Markus
1998-10-23, by paulson
export is_ml_identifier;
1998-10-23, by wenzelm
Updated to new datatype package.
1998-10-23, by berghofe
ex/Points added
1998-10-23, by narasche
Example for records
1998-10-23, by narasche
Directory Induct: Added new theory ABexp, removed obsolete
1998-10-23, by berghofe
Added new theory ABexp, removed obsolete theory Simult.
1998-10-23, by berghofe
Terms are now defined using the new datatype package.
1998-10-23, by berghofe
New example for using the datatype package:
1998-10-23, by berghofe
Removed obsolete theory Simult (see theory Term).
1998-10-23, by berghofe
started to add records;
1998-10-23, by wenzelm
occurs check now handles Bound variables (for soundness)
1998-10-23, by paulson
updated by isatool logo;
1998-10-23, by wenzelm
tuned block indent;
1998-10-22, by wenzelm
current_goals_markers;
1998-10-22, by wenzelm
some additions for Proof General by David Aspinall;
1998-10-22, by wenzelm
support current_goals_markers ref variable for print_current_goals;
1998-10-22, by wenzelm
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
1998-10-22, by wenzelm
fixed index.html;
1998-10-22, by wenzelm
tuned;
1998-10-22, by wenzelm
tuned;
1998-10-22, by wenzelm
standard Blast_tac demos
1998-10-22, by paulson
tidying
1998-10-22, by paulson
locales
1998-10-22, by paulson
Changed interface of inductive.
1998-10-21, by berghofe
Changed interface of rep_datatype: Characteristic theorems
1998-10-21, by berghofe
Changed interface.
1998-10-21, by berghofe
Changed interface of add_inductive: monos and con_defs are now
1998-10-21, by berghofe
Changed syntax of inductive.
1998-10-21, by berghofe
Changed syntax of rep_datatype and inductive: Theorems
1998-10-21, by berghofe
Added theorem prod_induct (needed for rep_datatype).
1998-10-21, by berghofe
Changed syntax of rep_datatype.
1998-10-21, by berghofe
fixed field_injects;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
no open;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
Tutorial
1998-10-21, by nipkow
dropped support for SML/NJ 109.x;
1998-10-21, by wenzelm
field_injects [iffs];
1998-10-21, by wenzelm
record_split_name;
1998-10-21, by wenzelm
tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-21, by wenzelm
improved var names;
1998-10-21, by wenzelm
tuned stack_overflow_handler;
1998-10-20, by wenzelm
made SML/NJ happy;
1998-10-20, by wenzelm
delSWrapper "record_split_tac";
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
split_paired_all.ML;
1998-10-20, by wenzelm
field types: datatype;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
quiet proofs;
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
Datatype instead of Prod;
1998-10-20, by wenzelm
QUIET_BREADTH_FIRST;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
simple Env replaced by Symtab;
1998-10-20, by wenzelm
added unvarify(T);
1998-10-20, by wenzelm
Syntax.max_pri;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
structure Hidden = struct end;
1998-10-20, by wenzelm
hiding private stuff;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
added foldl, keys;
1998-10-20, by wenzelm
split_paired_all.ML: turn surjective pairing into split rule;
1998-10-20, by wenzelm
updated
1998-10-20, by paulson
updated the MLWorks description
1998-10-20, by paulson
another little bug ;-) and minor changes in TLS.*;
1998-10-19, by mueller
little bug ;-)
1998-10-19, by mueller
added keyword 'and'
1998-10-19, by oheimb
corrected Header
1998-10-19, by oheimb
Addsimps [max_le_iff_conj];
1998-10-19, by nipkow
changed Super_L and Hyper_R to left and right Meta
1998-10-19, by oheimb
layout
1998-10-19, by oheimb
solved conflict by taking newest version;
1998-10-19, by mueller
added Clarify_tac to speed up proofs
1998-10-19, by paulson
moved a theorem
1998-10-19, by paulson
fixed comment
1998-10-19, by paulson
fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-10-19, by paulson
updated, tuned;
1998-10-18, by wenzelm
added Minho (Portugal);
1998-10-18, by wenzelm
Fixed bug (improper handling of flag flat_names).
1998-10-16, by berghofe
Added quiet_mode flag.
1998-10-16, by berghofe
- Changed structure of name spaces
1998-10-16, by berghofe
tuned MLWorks options;
1998-10-16, by wenzelm
MLWorks 2.0;
1998-10-16, by wenzelm
Changed structure of name spaces for datatypes.
1998-10-16, by berghofe
2. The simplifier now knows a little bit about nat-arithmetic.
1998-10-16, by nipkow
Mods because trans_tac is now part of thge simplifier.
1998-10-16, by nipkow
Mods because of: Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
1998-10-16, by paulson
parent is Main
1998-10-16, by paulson
*** empty log message ***
1998-10-16, by nipkow
integer simprocs
1998-10-15, by paulson
Uses overload_1st_set to specify overloading
1998-10-15, by paulson
specifications as sets of programs
1998-10-15, by paulson
Description of new version.
1998-10-14, by nipkow
New many-sorted version.
1998-10-14, by nipkow
See (* FIXME zero_neq_conv *)
1998-10-14, by nipkow
Nat: added zero_neq_conv
1998-10-14, by nipkow
added Int.int;
1998-10-13, by wenzelm
PRIVATE sig parts;
1998-10-13, by wenzelm
length_Suc_conv is no longer given to AddIffs
1998-10-13, by paulson
new theorems
1998-10-13, by paulson
tidied
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
new rule
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
Unified treatment of type error msgs.
1998-10-09, by nipkow
More pretty breaks in error msgs.
1998-10-09, by nipkow
Added a few breaks in error text.
1998-10-09, by nipkow
new theorem
1998-10-09, by paulson
new theorems
1998-10-09, by paulson
new guarantees laws
1998-10-09, by paulson
renamed Suc_card_Diff or something
1998-10-09, by nipkow
Multisets at last!
1998-10-09, by nipkow
added Induct/Multiset*
1998-10-09, by nipkow
New inductive definition of `card'
1998-10-09, by nipkow
polymorphic versions of nat_neq_iff and nat_neqE
1998-10-09, by paulson
Further improvement of the simplifier.
1998-10-08, by nipkow
Tuned simplifier not to re-normalized already normalized terms.
1998-10-07, by nipkow
tuned rm CVS;
1998-10-07, by wenzelm
runs test
1998-10-07, by nipkow
tidying and renaming
1998-10-07, by paulson
new theorems
1998-10-07, by paulson
tidied
1998-10-07, by paulson
new files UNITY/Comp.{thy,ML}
1998-10-07, by paulson
Merges FoldSet into Finite
1998-10-06, by nipkow
deleted incorrect code that set Goals.proof_timing:=false
1998-10-05, by paulson
Now prove_goalw_cterm never prints timing statistics
1998-10-05, by paulson
MLWorks demands the "op" before $
1998-10-05, by paulson
Finished proofs to end of section 5.1 of Chandy and Sanders
1998-10-05, by paulson
Join now an infix operator
1998-10-05, by paulson
simpler interface for Abel_Cancel
1998-10-05, by paulson
tidied
1998-10-05, by paulson
id <-> Id
1998-10-02, by nipkow
added Real to BasisLibrary
1998-10-02, by paulson
new file Provers/Arith/abel_cancel.ML
1998-10-02, by paulson
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
1998-10-02, by paulson
tidying
1998-10-02, by paulson
white border -- disabled;
1998-10-01, by wenzelm
Improved definition of foldSet.
1998-10-01, by nipkow
revised for new treatment of integers
1998-10-01, by paulson
new singleton_conv2
1998-10-01, by nipkow
tidied
1998-10-01, by paulson
a few new lemmas.
1998-10-01, by nipkow
composition theory
1998-10-01, by paulson
abstype of programs
1998-10-01, by paulson
now invokes functor
1998-10-01, by paulson
much tidying
1998-10-01, by paulson
new lemmas
1998-10-01, by paulson
better handling of literals
1998-10-01, by paulson
tidied
1998-10-01, by paulson
white space
1998-10-01, by paulson
new simproc functor
1998-10-01, by paulson
Revised version with Abelian group simprocs
1998-10-01, by paulson
handle empty name;
1998-09-29, by wenzelm
auto update
1998-09-29, by paulson
new function inter_term
1998-09-29, by paulson
Now id:(Acts prg) is implicit
1998-09-29, by paulson
modified proof for new simproc
1998-09-29, by paulson
many renamings and changes. Simproc for cancelling common terms in relations
1998-09-29, by paulson
New keywords
1998-09-29, by nipkow
Revised wf_acc_iff and Co.
1998-09-29, by nipkow
new: wfUNIVI
1998-09-29, by nipkow
Package now chooses type variable names more carefully to
1998-09-26, by berghofe
minor corrections
1998-09-25, by oheimb
exchanged automatic-tactics and semi-automatic-tactics
1998-09-25, by oheimb
improved indentation
1998-09-25, by oheimb
rearranged SIMPSET(');
1998-09-25, by wenzelm
*** empty log message ***
1998-09-25, by wenzelm
isatool logo;
1998-09-25, by wenzelm
added isatool logo;
1998-09-25, by wenzelm
improved;
1998-09-25, by wenzelm
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
added Int to BasisLibrary
1998-09-25, by paulson
deleted illegal "op"
1998-09-25, by paulson
uses BasisLibrary for Int.min
1998-09-25, by paulson
patched obsolete code
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*
1998-09-25, by paulson
Now uses integers instead of naturals
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
tuned;
1998-09-25, by wenzelm
tuned pretty_tag;
1998-09-25, by wenzelm
added REPEAT1;
1998-09-25, by wenzelm
create an instance of the Isabelle logo;
1998-09-24, by wenzelm
generic eps version;
1998-09-24, by wenzelm
simplified CLASIMP_DATA
1998-09-24, by oheimb
removed addcongs2 and delcongs2
1998-09-24, by oheimb
renamed mk_meta_eq to mk_eq
1998-09-24, by oheimb
simplified CLASIMP_DATA
1998-09-24, by oheimb
renamed some axioms; some new theorems
1998-09-24, by paulson
introduced addSE2, addSD2, addE2, and addD2
1998-09-24, by oheimb
improved description of looper and splitter
1998-09-24, by oheimb
workaround for litte bug in our ln command
1998-09-24, by oheimb
Function nat_of now maps negative integers to zero, not their absolute value
1998-09-24, by paulson
renamed some axioms
1998-09-24, by paulson
added correctness proofs for arithmetic
1998-09-24, by paulson
new induction rule for integers
1998-09-24, by paulson
fixed calls of ln, rm
1998-09-24, by oheimb
changed xnum token syntax;
1998-09-23, by wenzelm
unary minus
1998-09-23, by paulson
much renaming and reorganization
1998-09-23, by paulson
New directory Integ for the integers
1998-09-23, by paulson
a few new theorems
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tidying and deleting needless parentheses
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tuned Isamode;
1998-09-22, by wenzelm
re-organized for the new directory Integ
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
deleted erroneous semicolon
1998-09-22, by paulson
tidying
1998-09-22, by paulson
tidying
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
big tidying of simpsets, etc
1998-09-22, by paulson
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip