equal
deleted
inserted
replaced
439 ex/Group.ML ex/Group.thy ex/IntRing.ML ex/IntRing.thy \ |
439 ex/Group.ML ex/Group.thy ex/IntRing.ML ex/IntRing.thy \ |
440 ex/Lagrange.ML ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \ |
440 ex/Lagrange.ML ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \ |
441 ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \ |
441 ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \ |
442 ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \ |
442 ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \ |
443 ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \ |
443 ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \ |
444 ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy ex/Tuple.thy |
444 ex/Antiquote.thy ex/Multiquote.thy ex/Records.thy ex/Tuple.thy |
445 @$(ISATOOL) usedir $(OUT)/HOL ex |
445 @$(ISATOOL) usedir $(OUT)/HOL ex |
446 |
446 |
447 |
447 |
448 ## HOL-Isar_examples |
448 ## HOL-Isar_examples |
449 |
449 |