Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-240
+240
+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.
added length_Suc_conv, finite_set
1998-08-12, by oheimb
replaced idt by pttrn in @filter
1998-08-12, by oheimb
replaced split_etas by split_eta_proc
1998-08-12, by oheimb
added ospec
1998-08-12, by oheimb
minor correction: n must not be used as free variable
1998-08-12, by oheimb
eliminated fabs,fapp.
1998-08-12, by slotosch
suffix, unsuffix moved to Pure/library.ML;
1998-08-10, by wenzelm
fixed comment;
1998-08-10, by wenzelm
tuned;
1998-08-10, by wenzelm
??id syntax for text variables;
1998-08-10, by wenzelm
dest_binding, dest_skolem;
1998-08-10, by wenzelm
val single: 'a -> 'a list;
1998-08-10, by wenzelm
Tidying of AC, especially of AC16_WO4 using a locale
1998-08-10, by paulson
More lemmas about lex.
1998-08-10, by nipkow
*** empty log message ***
1998-08-08, by nipkow
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
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
1998-06-26, by paulson
fixed unit_eq;
1998-06-25, by wenzelm
delsimprocs [unit_eq_proc];
1998-06-25, by wenzelm
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
1998-06-25, by wenzelm
tuned loose bound vars check;
1998-06-25, by wenzelm
added unit_eq simplification procedure;
1998-06-25, by wenzelm
added XX_YY_rewrite: simpset -> cterm -> thm;
1998-06-25, by wenzelm
Thm.rewrite_cterm;
1998-06-25, by wenzelm
defaults for free variables hide consts of same name;
1998-06-25, by wenzelm
added rewrite_cterm;
1998-06-25, by wenzelm
Installation of target HOL-Real
1998-06-25, by paulson
* HOL/List: new function list_update written xs[i:=v] that updates the i-th
1998-06-24, by nipkow
Ran isatool fixgoal
1998-06-24, by paulson
removed duplicate entry for Goal
1998-06-24, by paulson
Trivial change to be more like paper
1998-06-24, by paulson
Tidying; renaming of Says_Server_message_form to
1998-06-24, by paulson
*** empty log message ***
1998-06-23, by nipkow
Consequences of the change from [ := ] to ( := ) in theory Update.
1998-06-23, by nipkow
Replaced [ := ] syntax by ( := ).
1998-06-23, by nipkow
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
1998-06-22, by paulson
comments and minor tidying
1998-06-22, by paulson
simplified and tidied the proofs
1998-06-22, by paulson
check_mlhome_file;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
isatool fixgoal;
1998-06-22, by wenzelm
def_sort;
1998-06-20, by wenzelm
renamed Thm(s) back to thm(s);
1998-06-20, by wenzelm
export mk_triple1/2;
1998-06-20, by wenzelm
added read_def_axm;
1998-06-20, by wenzelm
less
more
|
(0)
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip