HomeIsabelle/Phabricator
Diffusion afp-devel 802a16fc10b0

modify JinjaDCI
802a16fc10b0
Actions

Description

modify JinjaDCI

Details

Provenance
nanjiang <nanjiang@whu.edu.cn>Authored on
Parents
rAFPc5336131e4b5: modify JinjaDCI
rAFPe11414b94aae: Merged.
Branches
Unknown
Tags
Unknown

Event Timeline

nanjiang <nanjiang@whu.edu.cn> committed rAFP802a16fc10b0: modify JinjaDCI.Oct 22 2021, 5:05 PM

Merged Changes

Changes (201)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.
PathSize
metadata/
Akra_Bazzi/
Applicative_Lifting/
Auto2_HOL/
HOL/
Auto2_Imperative_HOL/
Imperative/
Automated_Stateful_Protocol_Verification/
trac/
Automatic_Refinement/
Lib/
Parametricity/
Tool/
Bernoulli/
Bertrands_Postulate/
Bicategory/
document/
Buffons_Needle/
Category3/
Collections/
ICF/
tools/
Comparison_Sort_Lower_Bound/
Conditional_Transfer_Rule/
CTR/
Tests/
UD/
Constructor_Funs/
Core_DOM/
common/
preliminaries/
Core_SC_DOM/
common/
preliminaries/
Deriving/
Comparator_Generator/
Equality_Generator/
Hash_Generator/
Descartes_Sign_Rule/
Dict_Construction/
E_Transcendental/
Generic_Deriving/
IMP2/
lib/
parser/
Impossible_Geometry/
Isabelle_C/
C11-FrontEnd/
examples/
src/
Isabelle_Meta_Model/
isabelle_home/
src/
Tools/
Code/
toy_example/
embedding/
Landau_Symbols/
Lazy_Case/
Linear_Recurrences/
Liouville_Numbers/
MFODL_Monitor_Optimized/
Minkowskis_Theorem/
Monad_Memo_DP/
transform/
Monad_Normalisation/
MonoidalCategory/
Myhill-Nerode/
Nominal2/
Partial_Function_MR/
Planarity_Certificates/
l4v/
lib/
wp/
Pratt_Certificate/
Prime_Harmonic_Series/
Proof_Strategy_Language/
Quick_Sort_Cost/
Random_BSTs/
Randomised_Social_Choice/
Automation/
Refine_Imperative_HOL/
Lib/
Refine_Monadic/
Generic/
Regular-Sets/
SDS_Impossibility/
Separation_Logic_Imperative_HOL/
Examples/
Show/
Simpl/
SpecCheck/
Dynamic/
Stream_Fusion_Code/
Sturm_Sequences/
Examples/
Lib/
document/
Triangle/
Types_To_Sets_Extension/
ETTS/
UTP/
toolkit/
utp/

rAFP802a16fc10b0

View Options

metadata/metadata

View Options

thys/Akra_Bazzi/Akra_Bazzi.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Library.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Method.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Real.thy

View Options

thys/Akra_Bazzi/Eval_Numeral.thy

View Options

thys/Akra_Bazzi/Master_Theorem.thy

View Options

thys/Akra_Bazzi/Master_Theorem_Examples.thy

View Options

thys/Akra_Bazzi/akra_bazzi.ML

View Options

thys/Applicative_Lifting/applicative.ML

View Options

thys/Auto2_HOL/HOL/acdata.ML

View Options

thys/Auto2_HOL/HOL/induct_outer.ML

View Options

thys/Auto2_HOL/consts.ML

View Options

thys/Auto2_HOL/items.ML

View Options

thys/Auto2_HOL/normalize.ML

View Options

thys/Auto2_HOL/proofsteps.ML

View Options

thys/Auto2_HOL/property.ML

View Options

thys/Auto2_HOL/util.ML

View Options

thys/Auto2_HOL/wellform.ML

View Options

thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML

View Options

thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML

View Options

thys/Automated_Stateful_Protocol_Verification/trac/trac.thy

View Options

thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy

View Options

thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy

View Options

thys/Automatic_Refinement/Lib/Named_Sorted_Thms.thy

View Options

thys/Automatic_Refinement/Lib/Refine_Util.thy

View Options

thys/Automatic_Refinement/Lib/Tagged_Solver.thy

View Options

thys/Automatic_Refinement/Parametricity/Param_Tool.thy

View Options

thys/Automatic_Refinement/Parametricity/Relators.thy

View Options

thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy

View Options

thys/Automatic_Refinement/Tool/Autoref_Phases.thy

View Options

thys/Bernoulli/Bernoulli.thy

View Options

thys/Bernoulli/Bernoulli_FPS.thy

View Options

thys/Bernoulli/Periodic_Bernpoly.thy

View Options

thys/Bertrands_Postulate/Bertrand.thy

View Options

thys/Bicategory/Bicategory.thy

View Options

thys/Bicategory/BicategoryOfSpans.thy

View Options

thys/Bicategory/Coherence.thy

View Options

thys/Bicategory/ConcreteBicategory.thy

View Options

thys/Bicategory/EquivalenceOfBicategories.thy

View Options

thys/Bicategory/InternalAdjunction.thy

View Options

thys/Bicategory/InternalEquivalence.thy

View Options

thys/Bicategory/Modification.thy

View Options

thys/Bicategory/Prebicategory.thy

View Options

thys/Bicategory/Pseudofunctor.thy

View Options

thys/Bicategory/PseudonaturalTransformation.thy

View Options

thys/Bicategory/SpanBicategory.thy

View Options

thys/Bicategory/Strictness.thy

View Options

thys/Bicategory/Subbicategory.thy

View Options

thys/Bicategory/Tabulation.thy

View Options

thys/Bicategory/document/root.tex

View Options

thys/Buffons_Needle/Buffons_Needle.thy

View Options

thys/Category3/BinaryFunctor.thy

View Options

thys/Category3/Category.thy

View Options

thys/Category3/EquivalenceOfCategories.thy

View Options

thys/Category3/Functor.thy

View Options

thys/Category3/FunctorCategory.thy

View Options

thys/Category3/Limit.thy

View Options

thys/Category3/NaturalTransformation.thy

View Options

thys/Category3/SetCat.thy

View Options

thys/Category3/SetCategory.thy

View Options

thys/Category3/Yoneda.thy

View Options

thys/Collections/ICF/tools/ICF_Tools.thy

View Options

thys/Collections/ICF/tools/Locale_Code.thy

View Options

thys/Collections/ICF/tools/Ord_Code_Preproc.thy

View Options

thys/Collections/ICF/tools/Record_Intf.thy

View Options

thys/Comparison_Sort_Lower_Bound/Comparison_Sort_Lower_Bound.thy

View Options

thys/Conditional_Transfer_Rule/CTR/CTR_Relators.ML

View Options

thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy

View Options

thys/Conditional_Transfer_Rule/UD/UD_Consts.ML

View Options

thys/Constructor_Funs/constructor_funs.ML

View Options

thys/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy

View Options

thys/Core_SC_DOM/common/preliminaries/Hiding_Type_Variables.thy

View Options

thys/Deriving/Comparator_Generator/comparator_generator.ML

View Options

thys/Deriving/Equality_Generator/equality_generator.ML

View Options

thys/Deriving/Hash_Generator/hash_generator.ML

View Options

thys/Deriving/derive_manager.ML

View Options

thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy

View Options

thys/Dict_Construction/class_graph.ML

View Options

thys/Dict_Construction/dict_construction.ML

View Options

thys/Dict_Construction/side_conditions.ML

View Options

thys/E_Transcendental/E_Transcendental.thy

View Options

thys/Generic_Deriving/derive_util.ML

View Options

thys/IMP2/lib/named_simpsets.ML

View Options

thys/IMP2/parser/Parser.thy

View Options

thys/Impossible_Geometry/Impossible_Geometry.thy

View Options

thys/Isabelle_C/C11-FrontEnd/examples/C1.thy

View Options

thys/Isabelle_C/C11-FrontEnd/examples/C2.thy

View Options

thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy

View Options

thys/Isabelle_C/C11-FrontEnd/src/C_Eval.thy

View Options

thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy

View Options

thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Annotation.thy

View Options

thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy

View Options

thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy

View Options

thys/Landau_Symbols/Group_Sort.thy

View Options

thys/Landau_Symbols/Landau_Library.thy

View Options

thys/Landau_Symbols/Landau_More.thy

View Options

thys/Landau_Symbols/Landau_Real_Products.thy

View Options

thys/Landau_Symbols/Landau_Simprocs.thy

View Options

thys/Landau_Symbols/landau_simprocs.ML

View Options

thys/Lazy_Case/lazy_case.ML

View Options

thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy

View Options

thys/Liouville_Numbers/Liouville_Numbers.thy

View Options

thys/Liouville_Numbers/Liouville_Numbers_Misc.thy

View Options

thys/MFODL_Monitor_Optimized/Formula.thy

View Options

thys/Minkowskis_Theorem/Minkowskis_Theorem.thy

View Options

thys/Monad_Memo_DP/transform/Transform_Data.ML

View Options

thys/Monad_Normalisation/monad_rules.ML

View Options

thys/MonoidalCategory/MonoidalCategory.thy

View Options

thys/Myhill-Nerode/Non_Regular_Languages.thy

View Options

thys/Nominal2/nominal_dt_data.ML

View Options

thys/Nominal2/nominal_function_common.ML

View Options

thys/Nominal2/nominal_thmdecls.ML

View Options

thys/Partial_Function_MR/partial_function_mr.ML

View Options

thys/Planarity_Certificates/l4v/lib/wp/WP-method.ML

View Options

thys/Pratt_Certificate/pratt.ML

View Options

thys/Prime_Harmonic_Series/Prime_Harmonic.thy

View Options

thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy

View Options

thys/Prime_Harmonic_Series/Squarefree_Nat.thy

View Options

thys/Proof_Strategy_Language/Isar_Interface.ML

View Options

thys/Quick_Sort_Cost/Quick_Sort_Average_Case.thy

View Options

thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy

View Options

thys/Random_BSTs/Random_BSTs.thy

View Options

thys/Randomised_Social_Choice/Automation/Preference_Profile_Cmd.thy

View Options

thys/Randomised_Social_Choice/Automation/SDS_Automation.thy

View Options

thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy

View Options

thys/Refine_Monadic/Generic/RefineG_Transfer.thy

View Options

thys/Refine_Monadic/Refine_Automation.thy

View Options

thys/Regular-Sets/Regexp_Constructions.thy

View Options

thys/SDS_Impossibility/SDS_Impossibility.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map_Impl.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Idioms.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Imp_List_Spec.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Imp_Map_Spec.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Open_List.thy

View Options

thys/Show/show_generator.ML

View Options

thys/Simpl/hoare.ML

View Options

thys/SpecCheck/Dynamic/dynamic_construct.ML

View Options

thys/Stream_Fusion_Code/stream_fusion.ML

View Options

thys/Sturm_Sequences/Examples/Sturm_Ex.thy

View Options

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

View Options

thys/Sturm_Sequences/Sturm.thy

View Options

thys/Sturm_Sequences/Sturm_Method.thy

View Options

thys/Sturm_Sequences/Sturm_Theorem.thy

View Options

thys/Sturm_Sequences/document/root_userguide.tex

View Options

thys/Triangle/Angles.thy

View Options

thys/Triangle/Triangle.thy

View Options

thys/Types_To_Sets_Extension/ETTS/ETTS_Substitution.ML

View Options

thys/UTP/toolkit/Total_Recall.ML

View Options

thys/UTP/utp/uexpr_rep_eq.ML

View Options

thys/Virtual_Substitution/DNF.thy

View Options

thys/Virtual_Substitution/DNFUni.thy

View Options

thys/Virtual_Substitution/Debruijn.thy

View Options

thys/Virtual_Substitution/EliminateVariable.thy

View Options

thys/Virtual_Substitution/EqualityVS.thy

View Options

thys/Virtual_Substitution/ExecutiblePolyProps.thy

View Options

thys/Virtual_Substitution/ExportProofs.thy

View Options

thys/Virtual_Substitution/Exports.thy

View Options

thys/Virtual_Substitution/GeneralVSProofs.thy

View Options

thys/Virtual_Substitution/Heuristic.thy

View Options

thys/Virtual_Substitution/HeuristicProofs.thy

View Options

thys/Virtual_Substitution/Infinitesimals.thy

View Options

thys/Virtual_Substitution/InfinitesimalsUni.thy

View Options

thys/Virtual_Substitution/LinearCase.thy

View Options

thys/Virtual_Substitution/LuckyFind.thy

View Options

thys/Virtual_Substitution/MPolyExtension.thy

View Options

thys/Virtual_Substitution/NegInfinity.thy

View Options

thys/Virtual_Substitution/NegInfinityUni.thy

View Options

thys/Virtual_Substitution/OptimizationProofs.thy

View Options

thys/Virtual_Substitution/Optimizations.thy

View Options

thys/Virtual_Substitution/PolyAtoms.thy

View Options

thys/Virtual_Substitution/PrettyPrinting.thy

View Options

thys/Virtual_Substitution/QE.thy

View Options

thys/Virtual_Substitution/QuadraticCase.thy

View Options

thys/Virtual_Substitution/README.txt

View Options

thys/Virtual_Substitution/ROOT

View Options

thys/Virtual_Substitution/Reindex.thy

View Options

thys/Virtual_Substitution/UniAtoms.thy

View Options

thys/Virtual_Substitution/VSAlgos.thy

View Options

thys/Virtual_Substitution/VSQuad.thy

View Options

thys/Virtual_Substitution/document/root.bib

View Options

thys/Virtual_Substitution/document/root.tex

View Options

web/entries/BenOr_Kozen_Reif.html

View Options

web/entries/Differential_Game_Logic.html

View Options

web/entries/Dominance_CHK.html

View Options

web/entries/Jinja.html

View Options

web/entries/List-Index.html

View Options

web/entries/Polynomials.html

View Options

web/entries/Virtual_Substitution.html

View Options

web/index.html

View Options

web/statistics.html

View Options

web/topics.html