(****************************************************************************** * Clean * * Copyright ( c ) 2018 - 2019 Universit é Paris - Saclay , Univ . Paris - Sud , France * * All rights reserved . * * Redistribution and use in source and binary forms , with or without * modification , are permitted provided that the following conditions are * met : * * * Redistributions of source code must retain the above copyright * notice , this list of conditions and the following disclaimer . * * * Redistributions in binary form must reproduce the above * copyright notice , this list of conditions and the following * disclaimer in the documentation and / or other materials provided * with the distribution . * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission . * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * " AS IS " AND ANY EXPRESS OR IMPLIED WARRANTIES , INCLUDING , BUT NOT * LIMITED TO , THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED . IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT , INDIRECT , INCIDENTAL , * SPECIAL , EXEMPLARY , OR CONSEQUENTIAL DAMAGES ( INCLUDING , BUT NOT * LIMITED TO , PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES ; LOSS OF USE , * DATA , OR PROFITS ; OR BUSINESS INTERRUPTION ) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY , WHETHER IN CONTRACT , STRICT LIABILITY , OR TORT * ( INCLUDING NEGLIGENCE OR OTHERWISE ) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE , EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE . theory Test_Cleanimports Clean_Symbex"HOL-Eisbach.Eisbach" begin method memory_theory = (simp only: memory_theory MonadSE.bind_assoc')method norm = (auto dest!: assert_D)end
Messung V0.5 in Prozent C=80 H=96 G=88
¤ Dauer der Verarbeitung: 0.3 Sekunden
¤ *© Formatika GbR, Deutschland
