HomeIsabelle/Phabricator
Diffusion Isabelle c2ee8d993d6a

clarified signature: more scalable operations;
c2ee8d993d6a
Actions

Description

clarified signature: more scalable operations;

Details

Provenance
makariusAuthored on
Parents
rISABELLE7829d6435c60: more scalable operations;
Branches
Unknown
Tags
Unknown

Changes (85)

PathSize
src/
Doc/
Implementation/
HOL/
Analysis/
Decision_Procs/
Eisbach/
Import/
Library/
Sum_of_Squares/
Matrix_LP/
Compute_Oracle/
Nominal/
Real_Asymp/
Statespace/
TPTP/
TPTP_Parser/
Tools/
Argo/
BNF/
Ctr_Sugar/
Function/
Lifting/
Meson/
Metis/
Predicate_Compile/
Qelim/
Quickcheck/
Quotient/
SMT/
Transfer/
Types_To_Sets/
Provers/
Arith/
Pure/
Isar/
Proof/
Tools/
Tools/
Code/
IsaPlanner/
ZF/
Tools/

rISABELLEc2ee8d993d6a

View Options

src/Doc/Implementation/Logic.thy

Loading...
View Options

src/HOL/Analysis/normarith.ML

Loading...
View Options

src/HOL/Decision_Procs/approximation.ML

Loading...
View Options

src/HOL/Decision_Procs/ferrante_rackoff.ML

Loading...
View Options

src/HOL/Decision_Procs/ferrante_rackoff_data.ML

Loading...
View Options

src/HOL/Decision_Procs/langford_data.ML

Loading...
View Options

src/HOL/Eisbach/eisbach_rule_insts.ML

Loading...
View Options

src/HOL/Eisbach/match_method.ML

Loading...
View Options

src/HOL/Import/import_rule.ML

Loading...
View Options

src/HOL/Library/Sum_of_Squares/positivstellensatz.ML

Loading...
View Options

src/HOL/Library/cconv.ML

Loading...
View Options

src/HOL/Library/old_recdef.ML

Loading...
View Options

src/HOL/Library/rewrite.ML

Loading...
View Options

src/HOL/Matrix_LP/Compute_Oracle/linker.ML

Loading...
View Options

src/HOL/Nominal/nominal_datatype.ML

Loading...
View Options

src/HOL/Nominal/nominal_fresh_fun.ML

Loading...
View Options

src/HOL/Nominal/nominal_inductive.ML

Loading...
View Options

src/HOL/Nominal/nominal_inductive2.ML

Loading...
View Options

src/HOL/Real_Asymp/multiseries_expansion.ML

Loading...
View Options

src/HOL/Statespace/distinct_tree_prover.ML

Loading...
View Options

src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML

Loading...
View Options

src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

Loading...
View Options

src/HOL/Tools/Argo/argo_real.ML

Loading...
View Options

src/HOL/Tools/Argo/argo_tactic.ML

Loading...
View Options

src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

Loading...
View Options

src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

Loading...
View Options

src/HOL/Tools/Function/partial_function.ML

Loading...
View Options

src/HOL/Tools/Function/relation.ML

Loading...
View Options

src/HOL/Tools/Lifting/lifting_bnf.ML

Loading...
View Options

src/HOL/Tools/Lifting/lifting_def.ML

Loading...
View Options

src/HOL/Tools/Lifting/lifting_term.ML

Loading...
View Options

src/HOL/Tools/Meson/meson.ML

Loading...
View Options

src/HOL/Tools/Meson/meson_clausify.ML

Loading...
View Options

src/HOL/Tools/Metis/metis_reconstruct.ML

Loading...
View Options

src/HOL/Tools/Predicate_Compile/core_data.ML

Loading...
View Options

src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

Loading...
View Options

src/HOL/Tools/Qelim/cooper.ML

Loading...
View Options

src/HOL/Tools/Quickcheck/random_generators.ML

Loading...
View Options

src/HOL/Tools/Quotient/quotient_tacs.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_normalize.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_replay.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_replay_methods.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_util.ML

Loading...
View Options

src/HOL/Tools/Transfer/transfer.ML

Loading...
View Options

src/HOL/Tools/coinduction.ML

Loading...
View Options

src/HOL/Tools/hologic.ML

Loading...
View Options

src/HOL/Tools/inductive_set.ML

Loading...
View Options

src/HOL/Tools/lin_arith.ML

Loading...
View Options

src/HOL/Tools/monomorph.ML

Loading...
View Options

src/HOL/Tools/numeral.ML

Loading...
View Options

src/HOL/Tools/numeral_simprocs.ML

Loading...
View Options

src/HOL/Tools/record.ML

Loading...
View Options

src/HOL/Tools/reification.ML

Loading...
View Options

src/HOL/Tools/sat.ML

Loading...
View Options

src/HOL/Tools/semiring_normalizer.ML

Loading...
View Options

src/HOL/Tools/split_rule.ML

Loading...
View Options

src/HOL/Types_To_Sets/unoverload_type.ML

Loading...
View Options

src/Provers/Arith/fast_lin_arith.ML

Loading...
View Options

src/Provers/hypsubst.ML

Loading...
View Options

src/Pure/Isar/class_declaration.ML

Loading...
View Options

src/Pure/Isar/code.ML

Loading...
View Options

src/Pure/Isar/element.ML

Loading...
View Options

src/Pure/Isar/expression.ML

Loading...
View Options

src/Pure/Isar/generic_target.ML

Loading...
View Options

src/Pure/Isar/obtain.ML

Loading...
View Options

src/Pure/Isar/subgoal.ML

Loading...
View Options

src/Pure/Proof/proof_checker.ML

Loading...
View Options

src/Pure/Tools/rule_insts.ML

Loading...
View Options

src/Pure/conjunction.ML

Loading...
View Options

src/Pure/drule.ML

Loading...
View Options

src/Pure/goal.ML

Loading...
View Options

src/Pure/more_thm.ML

Loading...
View Options

src/Pure/morphism.ML

Loading...
View Options

src/Pure/raw_simplifier.ML

Loading...
View Options

src/Pure/tactic.ML

Loading...
View Options

src/Pure/thm.ML

Loading...
View Options

src/Pure/variable.ML

Loading...
View Options

src/Tools/Code/code_preproc.ML

Loading...
View Options

src/Tools/IsaPlanner/rw_inst.ML

Loading...
View Options

src/Tools/coherent.ML

Loading...
View Options

src/Tools/induct.ML

Loading...
View Options

src/Tools/misc_legacy.ML

Loading...
View Options

src/Tools/nbe.ML

Loading...
View Options

src/ZF/Tools/cartprod.ML

Loading...
View Options

src/ZF/Tools/inductive_package.ML

Loading...