src/HOL/IMP/Compiler0.thy
changeset 36765 0c5a8df725de
parent 30952 7ab2716dd93b
child 39246 9e58f0499f57
equal deleted inserted replaced
36764:17427cf6fe95 36765:0c5a8df725de