HomeIsabelle/Phabricator
Diffusion afp-devel f879f9b59107

discontinued obsolete "val extend = I" for data slots;
f879f9b59107
Actions

Description

discontinued obsolete "val extend = I" for data slots;

Details

Provenance
makariusAuthored on
Parents
rAFP96076d0d60c2: tuned;
Branches
Unknown
Tags
Unknown

Changes (66)

PathSize
thys/
Applicative_Lifting/
Auto2_HOL/
HOL/
Auto2_Imperative_HOL/
Imperative/
Automated_Stateful_Protocol_Verification/
trac/
Automatic_Refinement/
Lib/
Parametricity/
Tool/
Collections/
ICF/
tools/
Conditional_Transfer_Rule/
CTR/
Tests/
UD/
Constructor_Funs/
Core_DOM/
common/
preliminaries/
Core_SC_DOM/
common/
preliminaries/
Deriving/
Comparator_Generator/
Equality_Generator/
Hash_Generator/
Dict_Construction/
Generic_Deriving/
IMP2/
lib/
parser/
Isabelle_C/
C11-FrontEnd/
examples/
src/
Isabelle_Meta_Model/
isabelle_home/
src/
Tools/
Code/
toy_example/
embedding/
Lazy_Case/
Monad_Memo_DP/
transform/
Monad_Normalisation/
Nominal2/
Partial_Function_MR/
Planarity_Certificates/
l4v/
lib/
wp/
Pratt_Certificate/
Proof_Strategy_Language/
Randomised_Social_Choice/
Automation/
Refine_Imperative_HOL/
Lib/
Refine_Monadic/
Generic/
Show/
Simpl/
SpecCheck/
Dynamic/
Stream_Fusion_Code/
Types_To_Sets_Extension/
ETTS/
UTP/
toolkit/
utp/

rAFPf879f9b59107

View Options

thys/Applicative_Lifting/applicative.ML

Loading...
View Options

thys/Auto2_HOL/HOL/acdata.ML

Loading...
View Options

thys/Auto2_HOL/HOL/induct_outer.ML

Loading...
View Options

thys/Auto2_HOL/consts.ML

Loading...
View Options

thys/Auto2_HOL/items.ML

Loading...
View Options

thys/Auto2_HOL/normalize.ML

Loading...
View Options

thys/Auto2_HOL/proofsteps.ML

Loading...
View Options

thys/Auto2_HOL/property.ML

Loading...
View Options

thys/Auto2_HOL/wellform.ML

Loading...
View Options

thys/Auto2_Imperative_HOL/Imperative/assn_matcher.ML

Loading...
View Options

thys/Auto2_Imperative_HOL/Imperative/sep_steps.ML

Loading...
View Options

thys/Automated_Stateful_Protocol_Verification/trac/trac.thy

Loading...
View Options

thys/Automatic_Refinement/Lib/Named_Sorted_Thms.thy

Loading...
View Options

thys/Automatic_Refinement/Lib/Tagged_Solver.thy

Loading...
View Options

thys/Automatic_Refinement/Parametricity/Param_Tool.thy

Loading...
View Options

thys/Automatic_Refinement/Parametricity/Relators.thy

Loading...
View Options

thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy

Loading...
View Options

thys/Automatic_Refinement/Tool/Autoref_Phases.thy

Loading...
View Options

thys/Collections/ICF/tools/Locale_Code.thy

Loading...
View Options

thys/Collections/ICF/tools/Ord_Code_Preproc.thy

Loading...
View Options

thys/Collections/ICF/tools/Record_Intf.thy

Loading...
View Options

thys/Conditional_Transfer_Rule/CTR/CTR_Relators.ML

Loading...
View Options

thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy

Loading...
View Options

thys/Conditional_Transfer_Rule/UD/UD_Consts.ML

Loading...
View Options

thys/Constructor_Funs/constructor_funs.ML

Loading...
View Options

thys/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy

Loading...
View Options

thys/Core_SC_DOM/common/preliminaries/Hiding_Type_Variables.thy

Loading...
View Options

thys/Deriving/Comparator_Generator/comparator_generator.ML

Loading...
View Options

thys/Deriving/Equality_Generator/equality_generator.ML

Loading...
View Options

thys/Deriving/Hash_Generator/hash_generator.ML

Loading...
View Options

thys/Deriving/derive_manager.ML

Loading...
View Options

thys/Dict_Construction/class_graph.ML

Loading...
View Options

thys/Dict_Construction/dict_construction.ML

Loading...
View Options

thys/Dict_Construction/side_conditions.ML

Loading...
View Options

thys/Generic_Deriving/derive_util.ML

Loading...
View Options

thys/IMP2/lib/named_simpsets.ML

Loading...
View Options

thys/IMP2/parser/Parser.thy

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

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

Loading...
View Options

thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic_sequential.thy

Loading...
View Options

thys/Lazy_Case/lazy_case.ML

Loading...
View Options

thys/Monad_Memo_DP/transform/Transform_Data.ML

Loading...
View Options

thys/Monad_Normalisation/monad_rules.ML

Loading...
View Options

thys/Nominal2/nominal_dt_data.ML

Loading...
View Options

thys/Nominal2/nominal_function_common.ML

Loading...
View Options

thys/Nominal2/nominal_thmdecls.ML

Loading...
View Options

thys/Partial_Function_MR/partial_function_mr.ML

Loading...
View Options

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

Loading...
View Options

thys/Pratt_Certificate/pratt.ML

Loading...
View Options

thys/Proof_Strategy_Language/Isar_Interface.ML

Loading...
View Options

thys/Randomised_Social_Choice/Automation/Preference_Profile_Cmd.thy

Loading...
View Options

thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy

Loading...
View Options

thys/Refine_Monadic/Generic/RefineG_Transfer.thy

Loading...
View Options

thys/Refine_Monadic/Refine_Automation.thy

Loading...
View Options

thys/Show/show_generator.ML

Loading...
View Options

thys/Simpl/hoare.ML

Loading...
View Options

thys/SpecCheck/Dynamic/dynamic_construct.ML

Loading...
View Options

thys/Stream_Fusion_Code/stream_fusion.ML

Loading...
View Options

thys/Types_To_Sets_Extension/ETTS/ETTS_Substitution.ML

Loading...
View Options

thys/UTP/toolkit/Total_Recall.ML

Loading...
View Options

thys/UTP/utp/uexpr_rep_eq.ML

Loading...