isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Toplevel.loop: explicit argument for secure loop, no warning on quit;
2007-12-04, by wenzelm
added Isar.secure_main;
2007-12-04, by wenzelm
added Tools/isabelle_process.ML;
2007-12-04, by wenzelm
isabelle process: replaced option -p by -W (process wrapper);
2007-12-04, by wenzelm
replaced option -p by -W (process wrapper);
2007-12-04, by wenzelm
\<chi> is now considered a letter;
2007-12-04, by wenzelm
symbol chi is also a letter;
2007-12-04, by wenzelm
improvements
2007-12-03, by obua
overloading target
2007-12-03, by haftmann
interface for unchecked definitions
2007-12-03, by haftmann
shifted "fun" command to Wellfounded_Relations
2007-12-03, by haftmann
updated
2007-12-03, by haftmann
Eliminated unused theorems minusinf_ex and minusinf_bex
2007-12-02, by chaieb
first working version of instance target
2007-11-30, by haftmann
interpretation for typedefs
2007-11-30, by haftmann
using intro_locales instead of unfold_locales if appropriate
2007-11-30, by haftmann
more canonical attribute application
2007-11-30, by haftmann
adjustions to due to instance target
2007-11-30, by haftmann
new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
2007-11-30, by krauss
*** empty log message ***
2007-11-30, by nipkow
added {#.,.,...#}
2007-11-30, by nipkow
tuned
2007-11-29, by haftmann
stripped down
2007-11-29, by haftmann
isabelle-process: option -p echos ISABELLE_PID;
2007-11-29, by wenzelm
commit: non-critical, otherwise session restart will result in deadlock!
2007-11-29, by wenzelm
instance command as rudimentary class target
2007-11-29, by haftmann
dropped dead code
2007-11-29, by haftmann
polyml: default heap size is back to -H 200 (people are still using
2007-11-28, by wenzelm
an example file for how to treat Felleisen-Hieb-style contexts
2007-11-28, by urbanc
removed (cf. object_logic.ML);
2007-11-28, by wenzelm
added base_sort;
2007-11-28, by wenzelm
removed typedecl.ML (cf. object_logic.ML);
2007-11-28, by wenzelm
ObjectLogic.typedecl;
2007-11-28, by wenzelm
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
2007-11-28, by wenzelm
simplified using sledgehammer
2007-11-28, by paulson
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
2007-11-28, by paulson
comment
2007-11-28, by paulson
(reverted to unnamed infix)
2007-11-28, by haftmann
simplified interpretations
2007-11-28, by haftmann
deleted looping code theorem
2007-11-28, by haftmann
to_set now applies collect_mem_simproc as well.
2007-11-28, by berghofe
naming policy for instances
2007-11-28, by haftmann
tuned interfaces of class module
2007-11-28, by haftmann
dropped dead code
2007-11-28, by haftmann
dropped legacy unnamed infix
2007-11-28, by haftmann
dropped implicit assumption proof
2007-11-28, by haftmann
dropped legacy ml bindings
2007-11-28, by haftmann
tuned titles;
2007-11-27, by wenzelm
moved titles;
2007-11-27, by wenzelm
tuned title;
2007-11-27, by wenzelm
tuned titles;
2007-11-27, by wenzelm
standard_parse_term: check ambiguous results without changing the result yet;
2007-11-27, by wenzelm
challenge by John Harrison: down to 12s (was 17s, was 75s);
2007-11-27, by wenzelm
Knaster_Tarski: turned into Isar statement, tuned proofs;
2007-11-27, by wenzelm
first_order_match now only calls loose_bvar when inside an abstraction.
2007-11-27, by berghofe
check_conv now only performs beta-eta-normalization when equations
2007-11-27, by berghofe
Optimized beta_norm: only tries to normalize term when it contains
2007-11-27, by berghofe
Better error messages for cterm_instantiate.
2007-11-27, by berghofe
some more lemmas due to Peter Lammich;
2007-11-26, by wenzelm
Peter Lammich: HOL-Lattice lemmas;
2007-11-26, by wenzelm

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle