Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. NEWS;
  3. miscellaneous examples and experiments for Isabelle/Pure;
  4. tuned comments;
  5. unused;
  6. clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
  7. NEWS;
  8. clarified signature: more scalable operations;
  9. more scalable operations;
  10. more scalable operations;
  11. clarified order of extra type variables, following names more often than occurrences;
  12. clarified signature; tuned;
  13. tuned;
  14. more scalable operations;
  15. omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
Changeset 74289:7492cd35782e by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 74288:1fc263b5aac1 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 74287:f79dfc7656ae by wenzelm:
miscellaneous examples and experiments for Isabelle/Pure;
The file was addedsrc/Pure/ex/Def.thy
The file was addedsrc/Pure/ex/Def_Examples.thy
The file was modified src/Pure/ROOT (diff)
Changeset 74286:641300b56ebe by wenzelm:
tuned comments;
The file was modified src/HOL/ROOT (diff)
The file was modified src/Pure/ROOT (diff)
Changeset 74285:6876e3d5e362 by wenzelm:
unused;
The file was modified src/Pure/Isar/specification.ML (diff)
Changeset 74284:8d1e27a23dd1 by wenzelm:
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
The file was modified src/Pure/Isar/generic_target.ML (diff)
Changeset 74283:019fe8238656 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 74282:c2ee8d993d6a by wenzelm:
clarified signature: more scalable operations;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/HOL/Analysis/normarith.ML (diff)
The file was modified src/HOL/Decision_Procs/approximation.ML (diff)
The file was modified src/HOL/Decision_Procs/ferrante_rackoff.ML (diff)
The file was modified src/HOL/Decision_Procs/ferrante_rackoff_data.ML (diff)
The file was modified src/HOL/Decision_Procs/langford_data.ML (diff)
The file was modified src/HOL/Eisbach/eisbach_rule_insts.ML (diff)
The file was modified src/HOL/Eisbach/match_method.ML (diff)
The file was modified src/HOL/Import/import_rule.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
The file was modified src/HOL/Library/cconv.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Library/rewrite.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/linker.ML (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Nominal/nominal_fresh_fun.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive2.ML (diff)
The file was modified src/HOL/Real_Asymp/multiseries_expansion.ML (diff)
The file was modified src/HOL/Statespace/distinct_tree_prover.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Function/relation.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_bnf.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_term.ML (diff)
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/core_data.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/Quotient/quotient_tacs.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_util.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
The file was modified src/HOL/Tools/coinduction.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/monomorph.ML (diff)
The file was modified src/HOL/Tools/numeral.ML (diff)
The file was modified src/HOL/Tools/numeral_simprocs.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/reification.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/HOL/Tools/split_rule.ML (diff)
The file was modified src/HOL/Types_To_Sets/unoverload_type.ML (diff)
The file was modified src/Provers/Arith/fast_lin_arith.ML (diff)
The file was modified src/Provers/hypsubst.ML (diff)
The file was modified src/Pure/Isar/class_declaration.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/obtain.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Proof/proof_checker.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/conjunction.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/tactic.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/variable.ML (diff)
The file was modified src/Tools/Code/code_preproc.ML (diff)
The file was modified src/Tools/IsaPlanner/rw_inst.ML (diff)
The file was modified src/Tools/coherent.ML (diff)
The file was modified src/Tools/induct.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
The file was modified src/Tools/nbe.ML (diff)
The file was modified src/ZF/Tools/cartprod.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
Changeset 74281:7829d6435c60 by wenzelm:
more scalable operations;
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/type_infer.ML (diff)
The file was modified src/Pure/variable.ML (diff)
Changeset 74280:7466b17b0820 by wenzelm:
more scalable operations;
The file was modified src/Pure/more_unify.ML (diff)
Changeset 74279:42db84eaee2d by wenzelm:
clarified order of extra type variables, following names more often than occurrences;
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/primitive_defs.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 74278:a123db647573 by wenzelm:
clarified signature;<br>tuned;
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/primitive_defs.ML (diff)
The file was modified src/Pure/term_items.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 74277:8cff7900871f by wenzelm:
tuned;
The file was modified src/Pure/Isar/expression.ML (diff)
Changeset 74276:57b323e20763 by wenzelm:
more scalable operations;
The file was modified src/Pure/Isar/expression.ML (diff)
Changeset 74275:aed955bb4cb1 by wenzelm:
omit obsolete field &quot;xs&quot;: originally from fd0f8fa2b6bd, but later unused;
The file was modified src/Pure/Isar/expression.ML (diff)