Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-120
+120
+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.
analz_mono_contra_tac was wrong
1997-11-21, by paulson
Deleted some useless comments
1997-11-21, by paulson
minor improvements of formulation and proofs
1997-11-21, by oheimb
corrected INDUCT_FILES
1997-11-21, by oheimb
$ISABELLE_HOME/src;
1997-11-20, by wenzelm
improved error msg;
1997-11-20, by wenzelm
removed old note;
1997-11-20, by wenzelm
adapted print methods;
1997-11-20, by wenzelm
improved theorems print method: transfer_sg;
1997-11-20, by wenzelm
init_data: improved print method;
1997-11-20, by wenzelm
removed data.ML (made part of sign.ML);
1997-11-20, by wenzelm
added type object = exn;
1997-11-20, by wenzelm
added transfer_sg;
1997-11-20, by wenzelm
fixed xstr token encoding;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
tuned infer_types interface;
1997-11-20, by wenzelm
moved Sign.print_sg to display.ML;
1997-11-20, by wenzelm
exported pretty_classrel, pretty_arity;
1997-11-20, by wenzelm
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
1997-11-20, by wenzelm
added implode_xstr: string list -> string, explode_xstr: string -> string list;
1997-11-20, by wenzelm
Now uses induct_tac
1997-11-20, by paulson
Updated the NatSum example
1997-11-20, by paulson
New, higher-level definition of \\out macro
1997-11-20, by paulson
Speeded up the proof of succ_lt_induct_lemma
1997-11-20, by paulson
Two new rewrites
1997-11-20, by paulson
Got rid of some slow deepen_tac calls
1997-11-20, by paulson
Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-20, by paulson
No more makeatletter/other
1997-11-20, by paulson
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
1997-11-18, by paulson
The dtac was discarding information, though apparently no proofs were hurt
1997-11-18, by paulson
Fixed bug in inst_split.
1997-11-18, by berghofe
improved big_rec_name lookup;
1997-11-17, by wenzelm
Updated comments. A bug causes MLWorks to use much
1997-11-17, by paulson
Rationalized error handling: if low-level tactic (depth_tac) cannot accept the
1997-11-17, by paulson
Tuned function mk_cntxt_splitthm.
1997-11-17, by berghofe
Removed
1997-11-16, by nipkow
Redesigned the decision procedures for (Abelian) groups and commutative rings.
1997-11-15, by nipkow
Added
1997-11-15, by nipkow
merge_refs: check for different versions of theories;
1997-11-14, by wenzelm
export read_raw_typ;
1997-11-13, by wenzelm
fixed record parser;
1997-11-13, by wenzelm
improved record syntax;
1997-11-13, by wenzelm
made SML/NJ happy;
1997-11-13, by wenzelm
added thin_refl to hyp_subst_tac
1997-11-12, by oheimb
refer to $ISABELLE_HOME/src;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
renamed to use.ML;
1997-11-12, by wenzelm
Redefine 'use' command in order to support path variable expansion,
1997-11-12, by wenzelm
adapted to new Use, File structs;
1997-11-12, by wenzelm
added path variables;
1997-11-12, by wenzelm
File system operations.
1997-11-12, by wenzelm
moved old file stuff from library.ML to Thy/browser_info.ML;
1997-11-12, by wenzelm
added file.ML, use.ML;
1997-11-12, by wenzelm
tuned warning msg;
1997-11-12, by wenzelm
major cleanup;
1997-11-12, by wenzelm
moved 'latex' from library.ML to goals.ML;
1997-11-12, by wenzelm
tuned prths;
1997-11-12, by wenzelm
structure BasisLibrary;
1997-11-12, by wenzelm
added Thy/file.ML, Thy/use.ML;
1997-11-12, by wenzelm
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
restored last version
1997-11-12, by oheimb
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
1997-11-12, by oheimb
renamed split_T_case_prem to split_T_case_asm
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
renamed split_prem_tac to split_asm_tac
1997-11-12, by oheimb
Fixed indentation
1997-11-11, by paulson
Rationalized the theorem if_image_distrib.
1997-11-11, by paulson
Fixed indentation
1997-11-11, by paulson
Fixed spelling error
1997-11-11, by paulson
Made some proofs more robust
1997-11-11, by paulson
Now applies "map negOfGoal" to lits when expanding haz rules.
1997-11-11, by paulson
ASCII-fied;
1997-11-10, by wenzelm
polished definition of find_index_eq
1997-11-10, by oheimb
check files for non-ASCII characters;
1997-11-10, by wenzelm
replaced 8bit characters
1997-11-10, by oheimb
fixed LAM<...> syntax;
1997-11-10, by wenzelm
fixed spelling;
1997-11-10, by wenzelm
added split_prem_tac
1997-11-07, by oheimb
changed libraray function find to find_index_eq, currying it
1997-11-07, by oheimb
added contrapos
1997-11-07, by oheimb
added contrapos2
1997-11-07, by oheimb
added exists_Const
1997-11-07, by oheimb
Each datatype t now proves a theorem split_t_case_prem
1997-11-07, by nipkow
Perl no longer optional;
1997-11-06, by wenzelm
deriv: eliminated references to theory;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
tuned;
1997-11-06, by wenzelm
hyp_subst_tac checks if the equality has type variables and uses a suitable
1997-11-06, by paulson
subgoal_tac displays a warning if the new subgoal has type variables
1997-11-06, by paulson
mkdir -p bin;
1997-11-05, by wenzelm
Tools/8bit: ./mk;
1997-11-05, by wenzelm
*** empty log message ***
1997-11-05, by oheimb
tuned;
1997-11-05, by wenzelm
abandoned generation of tmp files
1997-11-05, by oheimb
various improvements
1997-11-05, by oheimb
reflecting changes of isa2latex
1997-11-05, by oheimb
several minor improvements
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added ax2isa
1997-11-05, by oheimb
added isabelle14 and isabelle24
1997-11-05, by oheimb
removed gererated files
1997-11-05, by oheimb
added entry for manual
1997-11-05, by oheimb
*** empty log message ***
1997-11-05, by oheimb
Now introduces Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
Adapted to removal of UN1_I, etc
1997-11-05, by paulson
UNIV now a constant; UNION1, INTER1 now translations and no longer have
1997-11-05, by paulson
Expandshort; new theorem le_square
1997-11-05, by paulson
generalized UNION1 to UNION
1997-11-05, by paulson
Tidied Key_supply3
1997-11-05, by paulson
fixed comment
1997-11-05, by paulson
UNIV & UNION1
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
Ran expandshort, especially to introduce Safe_tac
1997-11-05, by paulson
adapted typed_print_translation;
1997-11-05, by wenzelm
tuned record_info;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted pure_trfunsT;
1997-11-05, by wenzelm
print translation: added show_sorts argument;
1997-11-05, by wenzelm
less
more
|
(0)
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip