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

removed obsolete store_thm(s), cf. functional versions in pure_thy.ML;
2008-03-29, by wenzelm
added generic_theory transaction;
2008-03-29, by wenzelm
commands 'use' and 'ML' now thy_decl;
2008-03-29, by wenzelm
removed obsolete use_XXX;
2008-03-29, by wenzelm
eliminated destructive/critical theorem database;
2008-03-29, by wenzelm
certify wrt. dynamic context;
2008-03-29, by wenzelm
added map_theory_result, map_proof_result;
2008-03-29, by wenzelm
certify wrt. dynamic context;
2008-03-29, by wenzelm
eliminated non-linear access to thy1 and thy12c;
2008-03-29, by wenzelm
replaced 'ML' by diagnostic 'ML_command';
2008-03-29, by wenzelm
updated generated file;
2008-03-29, by wenzelm
simplified PureThy.store_thm;
2008-03-29, by wenzelm
replaced 'ML_setup' by 'ML';
2008-03-29, by wenzelm
* Eliminated destructive theorem database.
2008-03-29, by wenzelm
eliminated quiete_mode ref (not really needed);
2008-03-29, by wenzelm
eliminated quiete_mode ref (turned into proper argument);
2008-03-29, by wenzelm
eliminated quiete_mode ref (unused);
2008-03-29, by wenzelm
eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
2008-03-29, by wenzelm
added forget_structure;
2008-03-28, by wenzelm
eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
2008-03-28, by wenzelm
ml_tactic: non-critical version via proof data and thread data;
2008-03-28, by wenzelm
NAMED_CRITICAL;
2008-03-28, by wenzelm
unfold_locales now part of default tactic
2008-03-28, by haftmann
import Main explicitly
2008-03-28, by haftmann
dropped now superfluous ad-hoc adaption
2008-03-28, by haftmann
not depends on Main any longer
2008-03-28, by haftmann
accomodated to sledgehammer theory dependency requirement
2008-03-28, by haftmann
only invoke interpret
2008-03-28, by haftmann
updated generated file;
2008-03-28, by wenzelm
Context.>> : operate on Context.generic;
2008-03-28, by wenzelm
avoid rebinding of existing facts;
2008-03-28, by wenzelm
some styling
2008-03-28, by haftmann
some styling
2008-03-28, by haftmann
some styling
2008-03-28, by haftmann
tuned proofs
2008-03-28, by urbanc
tuned;
2008-03-28, by wenzelm
updated dependencies;
2008-03-28, by wenzelm
reorganized signature of ML_Context;
2008-03-28, by wenzelm
remove commented text
2008-03-27, by huffman
avoid ambiguity of State.state vs. JVMType.state;
2008-03-27, by wenzelm
declare cont_lemmas_ext as simp rules individually
2008-03-27, by huffman
avoid amiguity of Continuity.chain vs. Porder.chain;
2008-03-27, by wenzelm
avoid amiguity of State.state vs. JVMType.state;
2008-03-27, by wenzelm
changed wrong assignement in signature sections
2008-03-27, by haftmann
clarified character serializations
2008-03-27, by haftmann
added Enum
2008-03-27, by haftmann
circumventing merge problem
2008-03-27, by haftmann
explicit case names for rule list_induct2
2008-03-27, by haftmann
instance for functions, explicit characters
2008-03-27, by haftmann
lemmas about map_of (zip _ _)
2008-03-27, by haftmann
restructuring; explicit case names for rule list_induct2
2008-03-27, by haftmann
no "attach UNIV" any more
2008-03-27, by haftmann
tuned comments;
2008-03-27, by wenzelm
tuned comments;
2008-03-27, by wenzelm
fixed theory imports;
2008-03-27, by wenzelm
tuned appendix;
2008-03-27, by wenzelm
removed obsolete appl_syntax, applC_syntax;
2008-03-27, by wenzelm
eliminated delayed theory setup
2008-03-27, by wenzelm
Command 'setup': discontinued implicit version.
2008-03-27, by wenzelm
eliminated theory ProtoPure;
2008-03-27, by wenzelm

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

isabelle