isabelle: Graph

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

moved markup.ML before position.ML;
2007-07-07, by wenzelm
The order for parameter for interpretation is now inversted:
2007-07-07, by chaieb
Common markup elements.
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
tuned;
2007-07-07, by wenzelm
simplified output mode setup;
2007-07-07, by wenzelm
added print_mode setup: indent and markup;
2007-07-07, by wenzelm
renamed raw to escape;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
added General/markup.ML;
2007-07-07, by wenzelm
added class skolem, command;
2007-07-07, by wenzelm
more interpretations
2007-07-06, by nipkow
Produce good PGML 2.0
2007-07-06, by aspinall
cosmetic (line length fixed)
2007-07-06, by webertj
Some examples for reifying type variables
2007-07-06, by chaieb
Tuned document
2007-07-06, by chaieb
Cleaned add and del attributes
2007-07-06, by chaieb
Reification now deals with type variables
2007-07-06, by chaieb
Cumulative reports for Poly/ML profiling output.
2007-07-06, by wenzelm
Update PGML version, add system name
2007-07-05, by aspinall
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
2007-07-05, by wenzelm
added type conv;
2007-07-05, by wenzelm
removed comments -- no exception TERM;
2007-07-05, by wenzelm
added is_reflexive;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
simplified has_meta_prems;
2007-07-05, by wenzelm
moved type conv to thm.ML;
2007-07-05, by wenzelm
the_theory/proof: error instead of exception Fail;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
renamed Conv.is_refl to Thm.is_reflexive;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
simplified ObjectLogic.atomize;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
Revert body of pgml to match schema for now [change bad for Broker]
2007-07-05, by aspinall
Classify -- comments as ordinary comments (no undo)
2007-07-05, by aspinall
tuned;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
sort_le: tuned eq case;
2007-07-05, by wenzelm
tuned goal conversion interfaces;
2007-07-05, by wenzelm
else_conv: only handle THM | CTERM | TERM | TYPE;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
2007-07-05, by wenzelm
Logical operations on numerals (see also HOL/hologic.ML).
2007-07-05, by wenzelm
added Tools/numeral.ML;
2007-07-05, by wenzelm
common normalizer_funs, avoid cterm_of;
2007-07-05, by wenzelm
Numeral.mk_cnumber;
2007-07-05, by wenzelm
PGML abstraction, draft version
2007-07-04, by aspinall
Use pgml
2007-07-04, by aspinall
fixed argument order in calls to Integer.pow
2007-07-04, by obua
added binop_cong_rule;
2007-07-04, by wenzelm
export dlo_conv;
2007-07-04, by wenzelm
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-04, by wenzelm
*** empty log message ***
2007-07-04, by nipkow
*** empty log message ***
2007-07-04, by nipkow
simplified a proof
2007-07-04, by paulson
tuned;
2007-07-03, by wenzelm
CONVERSION: handle TYPE | TERM | CTERM | THM;
2007-07-03, by wenzelm
proper use of ioa_package.ML;
2007-07-03, by wenzelm
tuned;
2007-07-03, by wenzelm
tuned is_comb/is_binop -- avoid construction of cterms;
2007-07-03, by wenzelm
HOLogic.conj_intr/elims;
2007-07-03, by wenzelm
use mucke_oracle.ML only once;
2007-07-03, by wenzelm
assume basic HOL context for compilation (antiquotations);
2007-07-03, by wenzelm
proper use of function_package ML files;
2007-07-03, by wenzelm
use hologic.ML in basic HOL context;
2007-07-03, by wenzelm
to handle non-atomic assumptions
2007-07-03, by paulson
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
2007-07-03, by wenzelm
convert instance proofs to Isar style
2007-07-03, by huffman
Dependency on reflection_data.ML to build HOL-ex
2007-07-03, by chaieb
Generalized case for atoms. Selection of environment lists is allowed more than once.
2007-07-03, by chaieb
More examples
2007-07-03, by chaieb
reflection and reification methods now manage Context data
2007-07-03, by chaieb
Context Data for the reflection and reification methods
2007-07-03, by chaieb
rename class dom to ring_1_no_zero_divisors
2007-07-03, by huffman
rewrite_goal_tac;
2007-07-03, by wenzelm
replaced Conv.goals_conv by Conv.prems_conv;
2007-07-03, by wenzelm
exported meta_rewrite_conv;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
removed obsolete eta_long_tac;
2007-07-03, by wenzelm
added CONVERSION tactical;
2007-07-03, by wenzelm
tuned rotate_prems;
2007-07-03, by wenzelm
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-07-03, by wenzelm
removed obsolete mk_conjunction_list, intr/elim_list;
2007-07-03, by wenzelm
removed obsolete goals_conv (cf. prems_conv);
2007-07-03, by wenzelm
Conjunction.intr/elim_balanced;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
Conjunction.mk_conjunction_balanced;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
Fixed problem with patterns in lambdas
2007-07-03, by nipkow
fixed an issue with mutual recursion
2007-07-03, by krauss
instance pordered_comm_ring < pordered_ring
2007-07-03, by huffman
Added pattern maatching for lambda abstraction
2007-07-02, by nipkow
revised the discussion of type classes
2007-07-02, by paulson
Generic QE need no Context anymore
2007-07-02, by chaieb
Handle exception TYPE
2007-07-02, by chaieb
Tuned proofs
2007-07-02, by chaieb
added ordered_ring and ordered_semiring
2007-06-30, by obua
tuned arithmetic modules
2007-06-29, by haftmann
bug fixes to proof reconstruction
2007-06-29, by paulson
dropped local cg cmd
2007-06-29, by haftmann
dropped toplevel lcm, gcd
2007-06-28, by haftmann
proper collapse_let
2007-06-28, by haftmann
new code generator framework
2007-06-28, by haftmann
dropped Library.lcm
2007-06-28, by haftmann
tuned
2007-06-28, by haftmann
code generation for dvd
2007-06-28, by haftmann
simplified keyword setup
2007-06-28, by haftmann
GPL -> BSD
2007-06-27, by paulson
*** empty log message ***
2007-06-27, by nipkow
updated for metis method
2007-06-26, by paulson
recoded
2007-06-26, by paulson
simplified
2007-06-26, by paulson