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

Update test for new parse result
2007-03-03, by aspinall
Add setproverflag, to replace other flag controls
2007-03-03, by aspinall
Add objtypes to openblock/closeblock and theory items (can be used to control folding).
2007-03-03, by aspinall
Add more attributes to openblock. Change theory item objtype field to proper objtype.
2007-03-03, by aspinall
Add Isabelle-specific objtypes
2007-03-03, by aspinall
Comment
2007-03-03, by aspinall
clarified code
2007-03-03, by haftmann
clarified error message
2007-03-03, by haftmann
moved instance option :: finite to Finite_Set.thy
2007-03-03, by haftmann
moved instance option :: finite here
2007-03-03, by haftmann
Fix idvalue output and PGML print mode raw encode/decode.
2007-03-03, by aspinall
permitting empty datatypes
2007-03-02, by haftmann
improved handling of nat numerals
2007-03-02, by haftmann
tuned code theorems for ord on integers
2007-03-02, by haftmann
simplified code generator setup
2007-03-02, by haftmann
tuned code theorems
2007-03-02, by haftmann
added add_numerals_of
2007-03-02, by haftmann
now using "class"
2007-03-02, by haftmann
using "fst" "snd" for Haskell code
2007-03-02, by haftmann
added code theorems for UNIV
2007-03-02, by haftmann
adjusted to latest changes
2007-03-02, by haftmann
new code theorems
2007-03-02, by haftmann
syntax for "class attach const"
2007-03-02, by haftmann
prefix of class interpretation not mandatory any longer
2007-03-02, by haftmann
Meson.is_fol_term now takes a theory as argument. Minor tidying.
2007-03-02, by paulson
New code to store theorem names in a concise form rather than as fully-qualified.
2007-03-02, by paulson
The first-order test now tests for the obscure case of a polymorphic constant like 1 being
2007-03-02, by paulson
abbrev: be permissive after transformation;
2007-02-28, by wenzelm
exported get_ss, map_ss;
2007-02-28, by wenzelm
tuned;
2007-02-28, by wenzelm
tuned ML setup;
2007-02-28, by wenzelm
added @{const_name}, @{const_syntax};
2007-02-28, by wenzelm
more cleanup
2007-02-28, by krauss
Add closeblock/openblock structure to proof-block commands
2007-02-28, by aspinall
Updated success string for Vampire.
2007-02-28, by paulson
Now outputs metis calls
2007-02-28, by paulson
added headers
2007-02-28, by krauss
cleanup, fixing sml/nj related problems
2007-02-28, by krauss
gensym: removed bits of dead code;
2007-02-28, by wenzelm
gensym no longer includes ' or _ in names (trailing _ is bad)
2007-02-27, by paulson
tuned document;
2007-02-27, by wenzelm
\usepackage{amssymb};
2007-02-27, by wenzelm
moved some non-kernel material to more_thm.ML;
2007-02-26, by wenzelm
removed obsolete eq_set;
2007-02-26, by wenzelm
Thm.internalK;
2007-02-26, by wenzelm
Further operations on type thm, outside the inference kernel.
2007-02-26, by wenzelm
added more_thm.ML;
2007-02-26, by wenzelm
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-26, by wenzelm
Added formalization of size-change principle (experimental).
2007-02-26, by krauss
added theorems_of;
2007-02-26, by wenzelm
removed obsolete theorem_space;
2007-02-26, by wenzelm
Added lemma lfp_const: "lfp (%x. t) = t
2007-02-26, by krauss
exported serializer parsers
2007-02-23, by haftmann
proper treatment of -> as type constructor
2007-02-23, by haftmann
tuned
2007-02-23, by haftmann
add_path for naming in proof contexts
2007-02-23, by haftmann
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-23, by haftmann
slightly tuned
2007-02-23, by haftmann
slight cleanup
2007-02-23, by haftmann
adjusted code lemmas
2007-02-23, by haftmann

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

isabelle