isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

no Toplevel.print for by, ., ..;
1999-04-27, by wenzelm
improved print_state;
1999-04-27, by wenzelm
verbose flag;
1999-04-27, by wenzelm
use_thy_only made pervasive;
1999-04-27, by wenzelm
added Isar_examples/NatSum.thy;
1999-04-27, by wenzelm
Old stuff.
1999-04-27, by nipkow
proper quiet_mode;
1999-04-27, by wenzelm
adapted add_inductive, add_record;
1999-04-27, by wenzelm
adapted add_inductive;
1999-04-27, by wenzelm
intrs attributes;
1999-04-27, by wenzelm
proper quiet_mode;
1999-04-27, by wenzelm
iff_add_global (from simpdata.ML);
1999-04-27, by wenzelm
support forward chaining;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
added Isar_examples/Cantor.ML;
1999-04-27, by wenzelm
hol_setup, simpdata_setup;
1999-04-27, by wenzelm
"iff" attribute;
1999-04-27, by wenzelm
hol_setup;
1999-04-27, by wenzelm
"!" made keyword;
1999-04-27, by wenzelm
opt_thm_name: name optional;
1999-04-27, by wenzelm
added oooo;
1999-04-27, by wenzelm
fixed a bug many years old in rule plusEC
1999-04-26, by paulson
tuned msgs;
1999-04-26, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
elaborated;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned antiquotations;
1999-04-23, by wenzelm
improved 'single' method;
1999-04-23, by wenzelm
added thus, hence;
1999-04-23, by wenzelm
added FINISHED, same_tac;
1999-04-23, by wenzelm
use /usr/share and /usr/bin;
1999-04-23, by wenzelm
Now for recdefs that omit the WF relation;
1999-04-23, by paulson
Now for recdefs that omit the WF relation
1999-04-23, by paulson
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
1999-04-23, by paulson
chgrp isabelle;
1999-04-23, by wenzelm
detailed proofs;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
oops;
1999-04-23, by wenzelm
fixed IO;
1999-04-22, by wenzelm
improved load paths;
1999-04-22, by wenzelm
single method: include not_elim, imp_elim;
1999-04-22, by wenzelm
more graceful handling of load paths;
1999-04-22, by wenzelm
improved auto dir handling;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
make Isabelle rpm packages for Linux/x86 from the distribution;
1999-04-22, by wenzelm
use_thy etc.: may specify path prefix, which is temporarily used as load path;
1999-04-22, by wenzelm
switch_theory: Context.pass;
1999-04-22, by wenzelm
recdef (TFL) now requires theory Recdef;
1999-04-22, by wenzelm
recdef requires theory Recdef;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
rep_datatype syntax: 'induction' instead of 'induct';
1999-04-22, by wenzelm
add_recdef: actual simpset;
1999-04-22, by wenzelm
recdef adapted to RecdefPackage.add_recdef;
1999-04-22, by wenzelm
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
1999-04-22, by wenzelm
added ex and Modelcheck
1999-04-22, by mueller
tuned;
1999-04-22, by wenzelm
added for mucke translation;
1999-04-22, by mueller
deleted some old examples in Modelcheck;
1999-04-22, by mueller
added translation from IOA to mucalculus and corresponding modelchecker examples;
1999-04-22, by mueller
moved this trivial example to new ex dir;
1999-04-22, by mueller
changed to include new subdirs ex and Modelcheck;
1999-04-22, by mueller
put types into "" because of signature clash;
1999-04-22, by mueller
added frontend syntax for IOA, moved trivial examples to folder ex;
1999-04-22, by mueller
added modelchecker mucke besides modelchecker eindhoven;
1999-04-22, by mueller
delete old files for adding second modelchecker connection;
1999-04-22, by mueller
$ML_HOME/.arch-n-opsys 2>/dev/null;
1999-04-21, by wenzelm
smlnj-110 setup made default;
1999-04-21, by wenzelm
/usr/share/smlnj/bin;
1999-04-21, by wenzelm
Isamode 2.6 requires patch;
1999-04-21, by wenzelm
added is_current;
1999-04-21, by wenzelm
fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;
1999-04-20, by wenzelm
temporarily fake quiet_mode;
1999-04-20, by wenzelm
temporarily reverted to 1.24;
1999-04-20, by wenzelm
IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
1999-04-20, by paulson
Main is the correct parent
1999-04-20, by paulson
new result extend_LeadsTo
1999-04-20, by paulson
should not refer to Datatype
1999-04-20, by paulson
addition of Kerberos IV example
1999-04-20, by paulson
tidied
1999-04-20, by paulson
improved usage;
1999-04-19, by wenzelm
loadpath replaced;
1999-04-16, by wenzelm
and_list;
1999-04-16, by wenzelm
lifted enum;
1999-04-16, by wenzelm
may specify induction predicates as well;
1999-04-16, by wenzelm
added Isar_examples;
1999-04-16, by wenzelm
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
1999-04-16, by wenzelm
lemmas about proper subset relation;
1999-04-16, by wenzelm
Proof by induction on types / set / functions.
1999-04-16, by wenzelm
print_datatypes;
1999-04-16, by wenzelm
added Tools/induct_method.ML;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/inductive' theory data;
1999-04-16, by wenzelm
Sign.base_name fid;
1999-04-16, by wenzelm
added incr_indexes, incr_indexes_wrt;
1999-04-16, by wenzelm
Proof mod.
1999-04-15, by nipkow
Added new thms.
1999-04-15, by nipkow
quiet_mode;
1999-04-14, by wenzelm
Tools/inductive_package.ML;
1999-04-14, by wenzelm
triple_swap;
1999-04-14, by wenzelm
Wrapper module for Konrad Slind's TFL package.
1999-04-14, by wenzelm
remoced old set_current_thy;
1999-04-14, by wenzelm
tuned messages;
1999-04-14, by wenzelm
intrs: names and atts;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
intrs: provide names and atts;
1999-04-14, by wenzelm
cleaned comments;
1999-04-14, by wenzelm
tuned;
1999-04-14, by wenzelm
fixed named type infixes (actual BUG!);
1999-04-14, by wenzelm
updated isatool install;
1999-04-13, by wenzelm
-p option;
1999-04-13, by wenzelm
adapted isatool install;
1999-04-13, by wenzelm
improved isatool install;
1999-04-13, by wenzelm
tuned;
1999-04-13, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
fixed @@;
1999-04-07, by wenzelm