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.
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
adapted syn_ext_trfunsT;
1997-11-05, by wenzelm
adapted extend_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
added TYPE syntax;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
adapted add_trfunsT;
1997-11-05, by wenzelm
fixed exception OPTION;
1997-11-05, by wenzelm
base root = "";
1997-11-05, by wenzelm
Added an alternativ version of AutoChopper and a theory for the conversion of
1997-11-05, by nipkow
removed redundant ball_image
1997-11-04, by oheimb
removed redundant ball_empty and bex_empty (see equalities.ML)
1997-11-04, by oheimb
added several theorems
1997-11-04, by oheimb
added the, option_map, and case analysis theorems
1997-11-04, by oheimb
added zip and nodup
1997-11-04, by oheimb
added theorems for Eps
1997-11-04, by oheimb
tuned usage;
1997-11-04, by wenzelm
HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04, by wenzelm
tuned to make non-Poly/MLs happy;
1997-11-04, by wenzelm
tuned 'records' stuff;
1997-11-04, by wenzelm
added pretty_ctyp;
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
type object = exn (enhance readability);
1997-11-04, by wenzelm
*** empty log message ***
1997-11-04, by oheimb
* removed "axioms" and "generated by" section
1997-11-04, by oheimb
simplified (and corrected) syntax definition of fapp
1997-11-04, by oheimb
data kinds 'datatypes', data kinds 'records' added
1997-11-04, by narasche
removed old datatype_info;
1997-11-04, by wenzelm
added Thy/path.ML;
1997-11-04, by wenzelm
Logic.loops -> Logic.rewrite_rule_ok
1997-11-04, by nipkow
logic: loops -> rewrite_rule_ok
1997-11-04, by nipkow
added path.ML;
1997-11-04, by wenzelm
added base;
1997-11-04, by wenzelm
Abstract algebra of file paths. External representation Unix-style.
1997-11-04, by wenzelm
tuned;
1997-11-04, by wenzelm
removed old thy data stuff;
1997-11-04, by wenzelm
fixed set_current_thy pattern;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-04, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
adapted to new datatypes thy info;
1997-11-03, by wenzelm
tuned;
1997-11-03, by wenzelm
datatypes;
1997-11-03, by wenzelm
nat datatype_info moved to Nat.thy;
1997-11-03, by wenzelm
added MLtext section;
1997-11-03, by wenzelm
added distinct_fst_string;
1997-11-03, by wenzelm
tuned: distinct_fst_string;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
export const_decls parser;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
CLASET';
1997-11-03, by wenzelm
moved cladata.ML, simpdata.ML to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
added claset thy_data;
1997-11-03, by wenzelm
added simpset thy_data;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
isatool fixclasimp;
1997-11-03, by wenzelm
added thy_data;
1997-11-03, by wenzelm
use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
1997-11-03, by wenzelm
adapted to new implicit simpset;
1997-11-03, by wenzelm
adapted to new implicit claset;
1997-11-03, by wenzelm
fixed thy dependencies;
1997-11-03, by wenzelm
aded thy_data;
1997-11-03, by wenzelm
HOL theory data.
1997-11-03, by wenzelm
added thy_data.ML;
1997-11-03, by wenzelm
new implicit simpset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
new implicit claset mechanism based on Sign.sg anytype data;
1997-11-03, by wenzelm
adapted to new implicit claset mechanism;
1997-11-03, by wenzelm
fix references to implicit claset and simpset;
1997-11-03, by wenzelm
do not overwrite backup files;
1997-11-03, by wenzelm
set_session renamed to add_session;
1997-11-03, by wenzelm
tuned error msg;
1997-11-03, by wenzelm
made SML/97 happy;
1997-11-03, by wenzelm
expand_option_bind -> split_option_bind
1997-11-03, by nipkow
expand_option_case -> split_option_case
1997-11-03, by nipkow
*** empty log message ***
1997-11-03, by nipkow
expand_list_case -> split_list_case
1997-11-03, by nipkow
Indexed split_t_case.
1997-11-02, by nipkow
Documented `split_t_case' thm genearted by datatype.
1997-11-02, by nipkow
Fixed comments
1997-11-01, by paulson
New treatment of overloading\!
1997-11-01, by paulson
New syntax function for types
1997-11-01, by paulson
Faster lexing
1997-11-01, by paulson
New way of referring to Basis Library
1997-11-01, by paulson
mended type constraint\!
1997-11-01, by paulson
Set.thy was too specific
1997-11-01, by paulson
New Blast_tac (and minor tidying...)
1997-11-01, by paulson
Auto update
1997-11-01, by paulson
propagate exn msg;
1997-11-01, by wenzelm
dup sections: warning instead of error;
1997-10-31, by wenzelm
Session, Context;
1997-10-31, by wenzelm
tuned;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-31, by wenzelm
*** empty log message ***
1997-10-31, by wenzelm
added str_of_sg: sg -> string;
1997-10-31, by wenzelm
added mixfix_args;
1997-10-30, by wenzelm
tuned thy_data;
1997-10-30, by wenzelm
tuned init_data;
1997-10-30, by wenzelm
added thy_data;
1997-10-30, by wenzelm
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
1997-10-30, by wenzelm
Modified trace output routines of simplifier.
1997-10-30, by nipkow
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
domain package:
1997-10-30, by oheimb
PureThy.add_store_defs_i, PureThy.add_store_axioms;
1997-10-30, by wenzelm
fixed try_dest_adm;
1997-10-30, by wenzelm
added adm.ML;
1997-10-30, by wenzelm
tuned;
1997-10-30, by wenzelm
tuned simp trace;
1997-10-30, by wenzelm
*** empty log message ***
1997-10-30, by nipkow
Removed spurious blank.
1997-10-30, by nipkow
Updated proofs
1997-10-30, by nipkow
For each datatype `t' there is now a theorem `split_t_case' of the form
1997-10-30, by nipkow
fixed spaces in qed;
1997-10-29, by wenzelm
debugging concerning sort variables
1997-10-29, by oheimb
PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i, PureThy.add_store_axioms_i;
1997-10-28, by wenzelm
PureThy.add_store_defs_i;
1997-10-28, by wenzelm
PureThy.add_store_axioms;
1997-10-28, by wenzelm
fixed qed;
1997-10-28, by wenzelm
do not change global_names flag;
1997-10-28, by wenzelm
restructured -- uses PureThy storage facilities;
1997-10-28, by wenzelm
added ignored_consts, thms_containing, add_store_axioms(_i),
1997-10-28, by wenzelm
always reload .ML *and* .thy file;
1997-10-28, by wenzelm
PureThy.add_store_defs, PureThy.add_store_axioms;
1997-10-28, by wenzelm
added ancestors;
1997-10-28, by wenzelm
added name_of_thm;
1997-10-28, by wenzelm
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
1997-10-28, by wenzelm
eq_thm moved to thm.ML;
1997-10-28, by wenzelm
add_store_axioms_i;
1997-10-28, by wenzelm
Added finite_UNION/SigmaI.
1997-10-28, by nipkow
oops;
1997-10-27, by wenzelm
renamed put_* to store_*;
1997-10-27, by wenzelm
flipped global_names default;
1997-10-27, by wenzelm
do not change global_names flag;
1997-10-27, by wenzelm
Isa94-2 instead of Isa95;
1997-10-27, by wenzelm
adapted domain and ax_ops package for name spaces
1997-10-27, by oheimb
made SML/NJ happy;
1997-10-27, by wenzelm
Deleted two needless theorems
1997-10-27, by paulson
internalized some names
1997-10-25, by oheimb
corrected two comments
1997-10-25, by oheimb
Added
1997-10-24, by nipkow
oops, swap warnings;
1997-10-24, by wenzelm
record: tuned output;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
ProtoPure.flexpair_def;
1997-10-24, by wenzelm
merge: default to ProtoPure.thy;
1997-10-24, by wenzelm
ProtoPure.thy etc.;
1997-10-24, by wenzelm
tuned names;
1997-10-24, by wenzelm
self_ref: check_stale;
1997-10-24, by wenzelm
eq_thm (from drule.ML);
1997-10-24, by wenzelm
added declared: T -> string -> bool;
1997-10-24, by wenzelm
Pure.thy;
1997-10-24, by wenzelm
ProtoPure.thy;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
removed add_thms_as_axms;
1997-10-24, by wenzelm
Init 'theorems' data. The Pure theories.
1997-10-24, by wenzelm
added pure_thy.ML;
1997-10-24, by wenzelm
tuned;
1997-10-24, by wenzelm
Modified comment.
1997-10-24, by nipkow
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-24, by nipkow
HOL/Map
1997-10-24, by nipkow
Added the new theory Map.
1997-10-24, by nipkow
added record section;
1997-10-23, by wenzelm
Sign.name_of;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
improved typ parser, exported;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
hide id, stamps;
1997-10-23, by wenzelm
Sign.stamp_names_of;
1997-10-23, by wenzelm
added sort_wrt;
1997-10-23, by wenzelm
fixed prune of hidden short names;
1997-10-23, by wenzelm
tuned;
1997-10-23, by wenzelm
tuned;
1997-10-22, by wenzelm
certify: check_stale;
1997-10-22, by wenzelm
improved handling of draft signatures / theories; draft thms (and
1997-10-21, by wenzelm
sg_ref: automatic adjustment of thms of draft theories;
1997-10-21, by wenzelm
commit;
1997-10-21, by wenzelm
made Poly/ML happy, but SML/NJ unhappy;
1997-10-21, by wenzelm
typo
1997-10-21, by nipkow
Corrected alphabetical order of entries in signature.
1997-10-21, by nipkow
Fixed the index entries for "recursion, general"
1997-10-21, by paulson
Many minor speedups:
1997-10-21, by paulson
New rewrite rules image_iff
1997-10-21, by paulson
Documented `addsplits'
1997-10-20, by nipkow
make SML/NJ happy;
1997-10-20, by wenzelm
rm IOA TLA;
1997-10-20, by wenzelm
tuned types;
1997-10-20, by wenzelm
tuned sig;
1997-10-20, by wenzelm
reset global_names;
1997-10-20, by wenzelm
set global_names;
1997-10-20, by wenzelm
replaced ops by consts;
1997-10-20, by wenzelm
removed Dlist;
1997-10-20, by wenzelm
\label{simp-chap} -> chap:simplification
1997-10-20, by nipkow
fixed goal_XXX;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
tuned;
1997-10-20, by wenzelm
adapted to qualified names;
1997-10-20, by wenzelm
lookup long names of types;
1997-10-20, by wenzelm
tuned qualified names;
1997-10-20, by wenzelm
less
more
|
(0)
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip