Changes

Summary

merged
prefer formal comments;
uniform inner and outer comments: isabelle update_cartouches -c;
prefer formal comments;
prefer formal comments;

Changeset 8728:656846d82369 by wenzelm: merged
Changeset 8727:9bc2a5d00cc2 by wenzelm: prefer formal comments;
The file was modified	`thys/AVL-Trees/AVL2.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Simulations.thy` (diff)
The file was modified	`thys/Abstract_Soundness/Infinite_Proof_Soundness.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Approximation.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Print.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/AF_Stream_Exec.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Hensel.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Mahler_Measure.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Polynomial_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Reconstruction.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_invariants.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/ISK.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Monadic_Language.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Coll_Test.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Nested_DFS.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArrayHashMap.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashMap.thy` (diff)
The file was modified	`thys/ConcurrentGC/MarkObject.thy` (diff)
The file was modified	`thys/ConcurrentGC/Model.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/Three_Step_MRU.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU_Vote_Opt.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing/Two_Step_Observing.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing_Quorums.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing_Quorums_Opt.thy` (diff)
The file was modified	`thys/Consensus_Refined/Refinement.thy` (diff)
The file was modified	`thys/Consensus_Refined/Same_Vote.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting_Opt.thy` (diff)
The file was modified	`thys/DFS_Framework/Impl/Data/Simple_Impl.thy` (diff)
The file was modified	`thys/DFS_Framework/Impl/Structural/Tailrec_Impl.thy` (diff)
The file was modified	`thys/DFS_Framework/Invars/DFS_Invars_Basic.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/Eg1Eg2RefinementSimple.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/EgHighBranchRevC.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/Gateway.thy` (diff)
The file was modified	`thys/GPU_Kernel_PL/KPL_wellformedness.thy` (diff)
The file was modified	`thys/Gabow_SCC/Find_Path_Impl.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_GBG.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_SCC.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Elgamal.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Hashed_Elgamal.thy` (diff)
The file was modified	`thys/GraphMarkingIBP/DSWMark.thy` (diff)
The file was modified	`thys/IP_Addresses/CIDR_Split.thy` (diff)
The file was modified	`thys/IP_Addresses/IP_Address_Parser.thy` (diff)
The file was modified	`thys/IP_Addresses/IP_Address_toString.thy` (diff)
The file was modified	`thys/IP_Addresses/IPv6.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/Imperative_Insertion_Sort.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Correctness.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Fail/Ports_Fail.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/SQRL_Shorewall/SQRL_2015_nospoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Output_Interface_Replace.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Transform.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Goto.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Stateful.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Fixed_Action.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Spec.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/LOFT/LinuxRouter_OpenFlow_Translation.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Documentation.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/LTL_Rabin_Impl.thy` (diff)
The file was modified	`thys/Latin_Square/Latin_Square.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/List2.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/ListInf.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/ListInf_Prefix.thy` (diff)
The file was modified	`thys/List_Update/TS.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Weak_Transition_System.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Distributed_WebApp.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Imaginary_Factory_Network.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Tainting/MeasrDroid.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/METASINVAR_SystemBoundary.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/PCF/PCF.thy` (diff)
The file was modified	`thys/PLM/TAO_2_Semantics.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory_2.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Promela/Promela.thy` (diff)
The file was modified	`thys/Promela/PromelaDatastructures.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Formulas.thy` (diff)
The file was modified	`thys/ROBDD/Level_Collapse.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecUnGr.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_WGraph.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Snippets/Sepref_Snip_Datatype.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Impl_Heapmap.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Misc.thy` (diff)
The file was modified	`thys/Routing/Linux_Router.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Circ_List.thy` (diff)
The file was modified	`thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy` (diff)
The file was modified	`thys/UPF/Monads.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Partitions.thy` (diff)
Changeset 8726:5e5c48e5c72f by wenzelm: uniform inner and outer comments: isabelle update_cartouches -c;
The file was modified	`thys/Key_Agreement_Strong_Adversaries/AuthenticationI.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/AuthenticationN.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Channels.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/IK.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_lemmas.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_symmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Infra.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Messages.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Payloads.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Refinement.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Runs.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Secrecy.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3_symmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3_symmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3_symmetric.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_enc.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_sig.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Agents.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Atoms.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Channels.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Infra.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Keys.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Message.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Refinement.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Runs.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/a0i_agree.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/a0n_agree.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/s0g_secrecy.thy` (diff)
Changeset 8725:4c384402fbdb by wenzelm: prefer formal comments;
The file was modified	`thys/Key_Agreement_Strong_Adversaries/AuthenticationI.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/AuthenticationN.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/IK.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_lemmas.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Payloads.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Refinement.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Secrecy.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl2.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_enc.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Auth_simple/m3_sig.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_kerberos.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m2_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Agents.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Refinement.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/a0i_agree.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/a0n_agree.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/s0g_secrecy.thy` (diff)
Changeset 8724:d2977e824cd2 by wenzelm: prefer formal comments;
The file was modified	`thys/Isabelle_Meta_Model/Init.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Meta_Isabelle.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Meta_SML.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Parser_init.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Printer_Isabelle.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Printer_Pure.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Printer_SML.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Core.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Init_rbt.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Printer.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/core/Core_init.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor1_access.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_META.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_Toy.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_Toy_extended.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Parser_META.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_META.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_Toy.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_Toy_extended.thy` (diff)