Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-192
+192
+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.
List now contains some lexicographic orderings.
1998-08-08, by nipkow
added store_tthm;
1998-08-06, by wenzelm
Improved well-formedness check.
1998-08-06, by berghofe
even more tidying of Goal commands
1998-08-06, by paulson
A higher-level treatment of LeadsTo, minimizing use of "reachable"
1998-08-06, by paulson
Simplified proof!!
1998-08-06, by nipkow
*** empty log message ***
1998-08-06, by nipkow
Lemma renamed in HOL.
1998-08-06, by nipkow
Added macro `termi'
1998-08-06, by nipkow
New lemmas in List and Lambda in IsaMakefile
1998-08-06, by nipkow
Removed duplicate thms (see comment to Arith.ML)
1998-08-06, by nipkow
Removed duplicate thms:
1998-08-06, by nipkow
Removed comments.
1998-08-06, by nipkow
even more tidying of Goal commands
1998-08-06, by paulson
disjointness
1998-08-06, by paulson
Now recognizes both {}= and ={}
1998-08-06, by paulson
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
1998-08-06, by paulson
New result from AC directory
1998-08-06, by paulson
added solve_tac;
1998-08-06, by wenzelm
New results from AC
1998-08-06, by paulson
First steps towards termination of simply typed terms.
1998-08-06, by nipkow
binding / skolem vars;
1998-08-06, by wenzelm
Null program and a few new results
1998-08-05, by paulson
Finished the example
1998-08-05, by paulson
Indentation, comments
1998-08-05, by paulson
Renamed equals0D to equals0E
1998-08-05, by paulson
Tidied
1998-08-05, by paulson
Removal of "disjoint" translation
1998-08-05, by paulson
New record type of programs
1998-08-05, by paulson
Union primitives and examples
1998-08-05, by paulson
tuned;
1998-08-04, by wenzelm
added LocaleGroup, PiSets examples;
1998-08-04, by wenzelm
added Open_locale, Close_locale;
1998-08-04, by wenzelm
added 'locale' section;
1998-08-04, by wenzelm
Locale.setup;
1998-08-04, by wenzelm
added export: thm -> thm;
1998-08-04, by wenzelm
moved print_goals to locale.ML;
1998-08-04, by wenzelm
added locale.ML;
1998-08-04, by wenzelm
added icons;
1998-08-04, by wenzelm
Renamed equals0D to equals0E
1998-08-04, by paulson
Renamed equals0D to equals0E; tidied
1998-08-04, by paulson
Constant "invariant" and new constrains_tac, ensures_tac
1998-08-04, by paulson
Tidying
1998-08-04, by paulson
Boolean quantification
1998-08-04, by paulson
Deleted the redundant rule mem_if
1998-08-04, by paulson
fixed disjount translation;
1998-08-04, by wenzelm
tuned comments;
1998-08-04, by wenzelm
Better comments
1998-08-03, by paulson
New rewrite rules for quantification over bounded UNIONs
1998-08-03, by paulson
Tidied; uses records
1998-07-31, by paulson
new theorems for partial funcs
1998-07-31, by paulson
Pretty.sym;
1998-07-31, by wenzelm
size / length: printable length;
1998-07-31, by wenzelm
isatool expandshort;
1998-07-31, by wenzelm
Removal of obsolete "open" commands from heads of .ML files
1998-07-31, by paulson
Replaced nat.exhaustion by nat.exhaust
1998-07-31, by berghofe
Removed HOL/IMP/Com.ML because it contained only an "open" declaration
1998-07-31, by paulson
tidied
1998-07-31, by paulson
Removal of obsolete "open" commands from heads of .ML files
1998-07-31, by paulson
Fixed primrec.
1998-07-30, by berghofe
Fixed primrec.
1998-07-30, by berghofe
made SML/NJ happy;
1998-07-30, by wenzelm
functorized Clasimp module;
1998-07-30, by wenzelm
fixed primrec;
1998-07-30, by wenzelm
tuned;
1998-07-30, by wenzelm
Equations are now stored in theory.
1998-07-30, by berghofe
Deleted obsolete comments.
1998-07-30, by berghofe
Adapted to new datatype package.
1998-07-30, by berghofe
Script that adapts theories and proof scripts to new datatype package.
1998-07-30, by berghofe
make_defs not marked as internal;
1998-07-30, by wenzelm
late setup of Pure and CPure;
1998-07-29, by wenzelm
removed global_names flag;
1998-07-28, by wenzelm
theory_of renamed to theory (and made public);
1998-07-28, by wenzelm
added Real structure (taken from SML/NJ basis lib);
1998-07-28, by wenzelm
tuned;
1998-07-28, by wenzelm
Tidied
1998-07-28, by paulson
Changed "goal" to "Goal"
1998-07-28, by paulson
Updated examples
1998-07-28, by paulson
A little quantifier duplication for IFOL
1998-07-27, by paulson
A few new lemmas by Mark Staples
1998-07-27, by paulson
tuned;
1998-07-27, by wenzelm
conversion bug in simpproc list_eq
1998-07-27, by nipkow
added ex/MonoidGroups (record example);
1998-07-24, by wenzelm
added type and update syntax;
1998-07-24, by wenzelm
added more_update;
1998-07-24, by wenzelm
update -> fun_upd
1998-07-24, by nipkow
Map.update -> map_upd, Unpdate.update -> fun_upd
1998-07-24, by nipkow
added internal;
1998-07-24, by wenzelm
Adapted to new datatype package.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Renamed '$' to 'Scons' because of clashes with constants of the same
1998-07-24, by berghofe
Added functions addIffs and delIffs which operate on clasimpsets.
1998-07-24, by berghofe
Added theorem distinct_lemma (needed for datatypes).
1998-07-24, by berghofe
Declaration of type 'nat' as a datatype (this allows usage of
1998-07-24, by berghofe
Removed nat_case, nat_rec, and natE (now provided by datatype
1998-07-24, by berghofe
Removed ThyData setup.
1998-07-24, by berghofe
Added theorem ex1_implies_ex.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Adapted to new datatype package.
1998-07-24, by berghofe
Removed old datatype package.
1998-07-24, by berghofe
New theory Datatype. Needed as an ancestor when defining datatypes.
1998-07-24, by berghofe
Added new function add_typedef_i_no_def which doesn't add
1998-07-24, by berghofe
Replaced Nat.thy by NatDef.thy because Nat.thy depends on
1998-07-24, by berghofe
New primrec function definition package
1998-07-24, by berghofe
New datatype definition package
1998-07-24, by berghofe
induct_tac -> exhaust_tac in 2 places.
1998-07-24, by nipkow
moved long_names / cond_extern to name_space.ML;
1998-07-22, by wenzelm
tuned;
1998-07-22, by wenzelm
tuned;
1998-07-21, by wenzelm
fixed eps/ps find;
1998-07-21, by wenzelm
fixed CVSROOT;
1998-07-21, by wenzelm
fixed isabelle logo;
1998-07-21, by wenzelm
library includes Isabelle version information;
1998-07-21, by wenzelm
isatool expandshort;
1998-07-21, by wenzelm
fixed isabelle logo;
1998-07-21, by wenzelm
SYNC;
1998-07-21, by wenzelm
added pdfsetup and isabelle logo;
1998-07-20, by wenzelm
SYNC;
1998-07-20, by wenzelm
Added acc_downwards
1998-07-20, by nipkow
Added simproc list_eq.
1998-07-20, by nipkow
Simplified last proof.
1998-07-18, by nipkow
ZF: Main, Update
1998-07-17, by paulson
added case_tac to be like HOL
1998-07-17, by paulson
added Main and Update
1998-07-17, by paulson
as in HOL
1998-07-17, by paulson
A stronger apply_0, and new thm domain_lam
1998-07-17, by paulson
added comments
1998-07-17, by paulson
tidying
1998-07-17, by paulson
now with Goal cmd
1998-07-17, by paulson
tidying
1998-07-16, by paulson
Got rid of obsolete "goal" commands.
1998-07-16, by paulson
Addition of "Theorem B" of Peter Andrews
1998-07-16, by paulson
Fixed bug in transform_rule.
1998-07-15, by berghofe
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
More tidying and removal of "\!\!... from Goal commands
1998-07-15, by paulson
@ -> $
1998-07-15, by nipkow
disjoint
1998-07-15, by nipkow
Minor tidying up.
1998-07-15, by nipkow
Removal of leading "\!\!..." from most Goal commands
1998-07-15, by paulson
new stac
1998-07-14, by paulson
CHANGED_GOAL added to declare a more robust stac
1998-07-14, by paulson
inj_on
1998-07-14, by nipkow
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
1998-07-14, by paulson
Corrected dead link.
1998-07-13, by nipkow
Huge tidy-up: removal of leading \!\!
1998-07-13, by paulson
massive tidying of proofs
1998-07-13, by paulson
renamed mutex to Acts
1998-07-13, by paulson
Replace awkward primrec by recdef.
1998-07-13, by nipkow
swapped condition in update_apply.
1998-07-13, by nipkow
isatool expandshort;
1998-07-12, by wenzelm
the distribution now includes Isabelle icons: see
1998-07-10, by wenzelm
added xpm icons;
1998-07-10, by wenzelm
Converted to Auto_tac
1998-07-06, by nipkow
several new basic modules made available for general use;
1998-07-03, by wenzelm
cleaned up;
1998-07-03, by wenzelm
theory Main includes everything;
1998-07-03, by wenzelm
reorganized the main HOL image;
1998-07-03, by wenzelm
stepping stones: Recdef, Main;
1998-07-03, by wenzelm
stepping stones;
1998-07-03, by wenzelm
removed duplicate thms;
1998-07-03, by wenzelm
moved String theory to main HOL;
1998-07-03, by wenzelm
Removed disjE from list of rules used to simplify elimination
1998-07-03, by berghofe
Removed leading !! in goals
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Removed leading !! in goals.
1998-07-03, by nipkow
Renamed expand_if to split_if and setloop split_tac to addsplits,
1998-07-02, by paulson
HACKED declaration of addsplits
1998-07-02, by paulson
Deleted leading parameters thanks to new Goal command
1998-07-02, by paulson
tuned comment;
1998-07-02, by wenzelm
Symbol.beginning;
1998-07-02, by wenzelm
Uncurried functions LeadsTo and reach
1998-07-02, by paulson
fixed Integ;
1998-07-02, by wenzelm
Adapted to new inductive definition package.
1998-07-01, by berghofe
Fixed bug (improper handling of flag no_ind).
1998-07-01, by berghofe
Replaced "use_dir" command by "use", because nested calls
1998-07-01, by berghofe
HOL-Real
1998-07-01, by paulson
tuned Inductive.thy;
1998-07-01, by wenzelm
added add_typedecls;
1998-07-01, by wenzelm
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Adapted to new inductive package.
1998-06-30, by berghofe
Removed obsolete comments.
1998-06-30, by berghofe
Removed old inductive definition package.
1998-06-30, by berghofe
Removed structure Prod_Syntax.
1998-06-30, by berghofe
Adapted to new inductive definition package.
1998-06-30, by berghofe
Moved most of the Prod_Syntax - stuff to HOLogic.
1998-06-30, by berghofe
Added additional theorems needed for inductive definitions.
1998-06-30, by berghofe
New inductive definition package
1998-06-30, by berghofe
added quick_and_dirty flag;
1998-06-30, by wenzelm
moved actual (C)Pure theories to pure.ML;
1998-06-29, by wenzelm
tuned transaction;
1998-06-29, by wenzelm
use_text: verbose flag;
1998-06-29, by wenzelm
less
more
|
(0)
-3000
-1000
-192
+192
+1000
+3000
+10000
+30000
tip